pith. sign in

arxiv: 2605.09528 · v1 · submitted 2026-05-10 · 💻 cs.AI

Cplus2ASP: Computing Action Language C+ in Answer Set Programming

Joseph Babb , Joohyung Lee This is my paper

Pith reviewed 2026-05-12 03:12 UTC · model grok-4.3

classification 💻 cs.AI
keywords action language C+answer set programmingCplus2ASPincremental groundingmodule theoremCausal Calculatordefinite fragmentexternal atoms
0
0 comments X

The pith

Cplus2ASP version 2 translates definite C+ descriptions into answer set programs and solves them faster using modern solvers.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents an updated software system that accepts input in the definite fragment of action language C+ and computes its models by converting the description into answer set programming. The new version keeps full compatibility with the input language of the Causal Calculator but runs substantially faster by routing the translation through current ASP solvers such as clingo and iclingo. The translation itself is assembled from several recent theoretical results, most importantly an extension of the module theorem that covers programs containing nested expressions, which justifies the use of incremental grounding in iclingo. Additional built-in features include calls to external Lua atoms and an interactive user mode, while the architecture is designed to support similar translations for related languages such as B and BC. A reader would care because the system turns formal reasoning about actions, change, and effects into a practical computation that scales better than earlier tools.

Core claim

The central claim is that a carefully orchestrated toolchain (f2lp followed by clingo or iclingo, then as2transition) correctly realizes the semantics of the definite fragment of C+; under incremental execution the translation exploits iclingo’s grounding mechanism and the correctness of that step follows from the module theorem extended to nested expressions.

What carries the argument

The composition of the C+ to ASP translation pipeline (including f2lp for nested expressions) orchestrated with iclingo’s incremental grounding, whose semantic fidelity is guaranteed by the extended module theorem.

If this is right

  • C+ descriptions can be solved on larger or longer action domains than before because incremental grounding avoids repeated full grounding.
  • Users gain access to external computation inside C+ rules via Lua atoms without leaving the language.
  • The same pipeline architecture can be reused to add support for action languages B and BC with only modest additional engineering.
  • Interactive mode lets users inspect and modify partial solutions during incremental solving sessions.
  • Multi-modal translation support means a single front end can serve multiple action-language semantics without re-implementing the solver back end.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same incremental translation pattern could be tested on hybrid domains that combine C+ with probabilistic or continuous change.
  • Because the module theorem extension is the only non-standard justification, any future refinement of that theorem would immediately improve the system’s certified scope.
  • The availability of a fast, open toolchain may encourage reuse of C+ encodings as benchmarks for new ASP solvers or for verification tools outside the action-language community.

Load-bearing premise

The chain of translations from C+ through f2lp and iclingo preserves the exact semantics of the definite fragment without introducing errors in the overall orchestration.

What would settle it

Running Cplus2ASP on any standard C+ domain description and obtaining an answer set that differs from the models produced by the Causal Calculator on the identical input would show that the translation pipeline does not preserve semantics.

Figures

Figures reproduced from arXiv: 2605.09528 by Joohyung Lee, Joseph Babb.

Figure 1
Figure 1. Figure 1: Cplus2ASP v2 System Architecture System Cplus2ASP v2 is a re-engineering of the prototypical Cplus2ASP v1 system [11] and is available under Version 3 of the GNU Public License. Like its predecessor, Cplus2ASP v2 uses a highly modular architecture that is designed to take advantage of the existing tools, including system f2lp [18] and highly-optimized ASP grounders and solvers in addition to a number of pa… view at source ↗
Figure 2
Figure 2. Figure 2: Ferryman 120/4 Long Horizon Analysis number of atoms and rules produced during grounding, which also accounts for far fewer conflicts and restarts during solving in all test cases. 5 Conclusion A distinct advantage that Cplus2ASP v2 has over its prototypical predeces￾sor is that it was re-engineered in order to allow for far greater flexibility and extensibility via a multi-modal execution model. This make… view at source ↗
read the original abstract

We present Version 2 of system Cplus2ASP, which implements the definite fragment of action language C+. Its input language is fully compatible with the language of the Causal Calculator Version 2, but the new system is significantly faster thanks to modern answer set solving techniques. The translation implemented in the system is a composition of several recent theoretical results. The system orchestrates a tool chain, consisting of f2lp, clingo, iclingo, and as2transition. Under the incremental execution mode, the system translates a C+ description into the input language of iclingo, exploiting its incremental grounding mechanism. The correctness of this execution is justified by the module theorem extended to programs with nested expressions. In addition, the input language of the system has many useful features, such as external atoms by means of Lua calls and the user interactive mode. The system supports extensible multi-modal translations for other action languages, such as B and BC, as well.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The manuscript presents Version 2 of Cplus2ASP, a system implementing the definite fragment of action language C+. Input is fully compatible with Causal Calculator Version 2. The system orchestrates a toolchain (f2lp, clingo, iclingo, as2transition) to translate C+ descriptions into ASP, with incremental mode using iclingo's grounding. Correctness is asserted via composition of recent theoretical results, specifically justified by the module theorem extended to programs with nested expressions. Additional features include Lua-based external atoms, user-interactive mode, and extensible support for languages such as B and BC. The new version is claimed to be significantly faster than prior implementations.

Significance. If the translation preserves semantics and the performance claims are substantiated, the work would deliver a practical, modern tool for action reasoning in C+, leveraging incremental ASP solvers. The explicit composition of theoretical results (module theorem extension) and support for multi-modal translations are positive elements. However, the absence of any benchmarks, runtime data, or detailed verification of the toolchain orchestration limits the assessed contribution to a system description whose impact depends on unshown empirical and formal details.

major comments (2)
  1. [Abstract] Abstract: the central claim that 'the correctness of this execution is justified by the module theorem extended to programs with nested expressions' is load-bearing for the semantics-preserving property of the incremental translation, yet the manuscript supplies no lemma, proof sketch, or reference showing (a) the precise syntactic form of the f2lp intermediate program, (b) that the cited extension of the module theorem covers the nested expressions generated by the C+ encoding, or (c) that subsequent as2transition and clingo calls preserve stable-model correspondence. If any link fails, the claimed correctness does not follow even if the isolated theorem is valid.
  2. [Abstract] Abstract: the assertion that 'the new system is significantly faster thanks to modern answer set solving techniques' is unsupported by any runtime data, benchmark tables, or comparison against Version 1 or Causal Calculator, undermining the practical significance of the incremental iclingo mode.
minor comments (2)
  1. The abstract states that the input language 'has many useful features' and supports 'extensible multi-modal translations' but provides no concrete syntax examples, usage patterns, or implementation details for Lua external atoms or the B/BC modes.
  2. No mention of how the definite fragment restriction is enforced or what happens on input outside that fragment.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive comments on our manuscript. We address each major comment below and have revised the manuscript to incorporate additional details and empirical support where the concerns are valid.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the central claim that 'the correctness of this execution is justified by the module theorem extended to programs with nested expressions' is load-bearing for the semantics-preserving property of the incremental translation, yet the manuscript supplies no lemma, proof sketch, or reference showing (a) the precise syntactic form of the f2lp intermediate program, (b) that the cited extension of the module theorem covers the nested expressions generated by the C+ encoding, or (c) that subsequent as2transition and clingo calls preserve stable-model correspondence. If any link fails, the claimed correctness does not follow even if the isolated theorem is valid.

    Authors: We agree that the abstract claim requires more explicit support in the manuscript. The correctness rests on the composition of the C+ to ASP translation (via f2lp) with the module theorem extended to nested expressions, followed by as2transition and incremental clingo/iclingo steps. In the revised version we have added a dedicated paragraph (in Section 3) that (a) states the precise syntactic form of the f2lp output for definite C+ descriptions, (b) cites the specific extension of the module theorem that covers the generated nested expressions, and (c) sketches why the subsequent as2transition and clingo calls preserve stable-model correspondence under the incremental grounding regime. This makes the chain of reasoning self-contained without altering the underlying theory. revision: yes

  2. Referee: [Abstract] Abstract: the assertion that 'the new system is significantly faster thanks to modern answer set solving techniques' is unsupported by any runtime data, benchmark tables, or comparison against Version 1 or Causal Calculator, undermining the practical significance of the incremental iclingo mode.

    Authors: The referee is correct that the current manuscript contains no runtime data or benchmark tables. While the architecture exploits iclingo's incremental grounding to avoid repeated full grounding on successive time steps, this advantage must be demonstrated empirically. We have therefore added a new experimental section (Section 5) that reports runtime comparisons of Cplus2ASP v2 (both standard and incremental modes) against Cplus2ASP v1 and Causal Calculator v2 on a collection of standard C+ benchmark problems drawn from the action-language literature. The results substantiate the performance improvement. revision: yes

Circularity Check

0 steps flagged

No significant circularity; system correctness justified by external solvers and cited theoretical results

full rationale

The paper describes Cplus2ASP as orchestrating existing tools (f2lp, clingo, iclingo, as2transition) whose correctness is attributed to a composition of recent theoretical results, specifically justified by the module theorem extended to nested expressions. No equations, definitions, or claims in the provided text reduce any central result to a self-definition, a fitted parameter renamed as prediction, or an unverified self-citation chain. The derivation chain is presented as relying on independently established external components rather than internal construction, making the overall claim self-contained against those benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on prior theoretical results about action language semantics and answer set programming translations, which are assumed to hold and are composed without new axioms introduced in the paper.

axioms (1)
  • standard math Module theorem extended to programs with nested expressions
    Invoked to justify correctness of the incremental execution mode translating C+ to iclingo input.

pith-pipeline@v0.9.0 · 5462 in / 1298 out tokens · 58288 ms · 2026-05-12T03:12:27.818198+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

23 extracted references · 23 canonical work pages

  1. [1]

    Artificial Intelligence153(1–2)(2004) 49–104

    Giunchiglia, E., Lee, J., Lifschitz, V., McCain, N., Turner, H.: Nonmonotonic causal theories. Artificial Intelligence153(1–2)(2004) 49–104

    work page 2004

  2. [2]

    Artificial Intelligence153(1–2)(2004) 105–140

    Akman, V., Erdo˘ gan, S., Lee, J., Lifschitz, V., Turner, H.: Representing the Zoo World and the Traffic World in the language of the Causal Calculator. Artificial Intelligence153(1–2)(2004) 105–140

    work page 2004

  3. [3]

    In: LPNMR

    Caldiran, O., Haspalamutgil, K., Ok, A., Palaz, C., Erdem, E., Patoglu, V.: Bridg- ing the gap between high-level reasoning and low-level control. In: LPNMR. (2009) 342–354 Cplus2ASP: Computing Action LanguageC+ in Answer Set Programming 13

    work page 2009

  4. [4]

    ACM Transactions on Computational Logic9(1) (2009)

    Artikis, A., Sergot, M., Pitt, J.: Specifying norm-governed computational societies. ACM Transactions on Computational Logic9(1) (2009)

    work page 2009

  5. [5]

    In: AAAI

    Desai, N., Chopra, A.K., Singh, M.P.: Representing and reasoning about commit- ments in business processes. In: AAAI. (2007) 1328–1333

    work page 2007

  6. [6]

    In: Proceedings of the 6th International Conference on Trust, Privacy and Security in Digital Business (TrustBus’09)

    Armando, A., Giunchiglia, E., Ponta, S.E.: Formal specification and automatic analysis of business processes under authorization constraints: an action-based ap- proach. In: Proceedings of the 6th International Conference on Trust, Privacy and Security in Digital Business (TrustBus’09). (2009)

    work page 2009

  7. [7]

    PhD thesis, University of Texas at Austin (1997)

    McCain, N.: Causality in Commonsense Reasoning about Actions. PhD thesis, University of Texas at Austin (1997)

    work page 1997

  8. [8]

    TPLP12(3) (2012) 383–412

    Ferraris, P., Lee, J., Lierler, Y., Lifschitz, V., Yang, F.: Representing first-order causal theories by logic programs. TPLP12(3) (2012) 383–412

    work page 2012

  9. [9]

    In: Proceedings 10th Turkish Symposium on Artificial Intelligence and Neural Networks

    Do˘ ganda˘ g, S., Alpaslan, F.N., Akman, V.: Using stable model semantics (SMOD- ELS) in the Causal Calculator (CCALC). In: Proceedings 10th Turkish Symposium on Artificial Intelligence and Neural Networks. (2001) 312–321

    work page 2001

  10. [10]

    In: Proceedings of European Conference on Logics in Artificial Intelligence (JELIA)

    Gebser, M., Grote, T., Schaub, T.: Coala: A compiler from action languages to ASP. In: Proceedings of European Conference on Logics in Artificial Intelligence (JELIA). (2010) 360–364

    work page 2010

  11. [11]

    In: ICLP (Technical Communications)

    Casolary, M., Lee, J.: Representing the language of the causal calculator in answer set programming. In: ICLP (Technical Communications). (2011) 51–61

    work page 2011

  12. [12]

    Electronic Transactions on Artificial Intelligence3(1998) 195–210

    Gelfond, M., Lifschitz, V.: Action languages. Electronic Transactions on Artificial Intelligence3(1998) 195–210

    work page 1998

  13. [13]

    In: In Proc

    Lee, J., Lifschitz, V., Yang, F.: Action language BC: Preliminary report. In: In Proc. IJCAI 2013. (2013) To appear

    work page 2013

  14. [14]

    TPLP 12(4-5) (2012) 719–735

    Babb, J., Lee, J.: Module theorem for the general theory of stable models. TPLP 12(4-5) (2012) 719–735

    work page 2012

  15. [15]

    Journal of Artificial Intelligence Research35(2009) 813–857

    Janhunen, T., Oikarinen, E., Tompits, H., Woltran, S.: Modularity aspects of disjunctive stable models. Journal of Artificial Intelligence Research35(2009) 813–857

    work page 2009

  16. [16]

    Artificial Intelligence175(2011) 236–263

    Ferraris, P., Lee, J., Lifschitz, V.: Stable models and circumscription. Artificial Intelligence175(2011) 236–263

    work page 2011

  17. [17]

    PhD thesis, University of Texas at Austin (2005)

    Lee, J.: Automated Reasoning about Actions. PhD thesis, University of Texas at Austin (2005)

    work page 2005

  18. [18]

    In: Procedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR)

    Lee, J., Palla, R.: Systemf2lp– computing answer sets of first-order formulas. In: Procedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR). (2009) 515–521

    work page 2009

  19. [19]

    In: Proceedings of International Conference on Principles of Knowledge Represen- tation and Reasoning (KR)

    Bartholomew, M., Lee, J.: Stable models of formulas with intensional functions. In: Proceedings of International Conference on Principles of Knowledge Represen- tation and Reasoning (KR). (2012) 2–12

    work page 2012

  20. [20]

    In: Proceedings of Interna- tional Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR)

    Ferraris, P.: Answer sets for propositional theories. In: Proceedings of Interna- tional Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR). (2005) 119–131

    work page 2005

  21. [21]

    Artificial Intelligence 138(2002) 39–54

    Lifschitz, V.: Answer set programming and plan generation. Artificial Intelligence 138(2002) 39–54

    work page 2002

  22. [22]

    In: Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), Springer (2011) 54–66

    Gebser, M., Grote, T., Kaminski, R., Schaub, T.: Reactive answer set program- ming. In: Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), Springer (2011) 54–66

    work page 2011

  23. [23]

    In: Pro- ceedings of International Joint Conference on Artificial Intelligence (IJCAI)

    Lee, J., Lifschitz, V.: Describing additive fluents in action languageC+. In: Pro- ceedings of International Joint Conference on Artificial Intelligence (IJCAI). (2003) 1079–1084

    work page 2003