LLM+AL: Bridging Large Language Models and Action Languages for Complex Reasoning about Actions

Adam Ishay; Joohyung Lee

REVIEW 3 major objections 5 minor 25 references

LLM+AL: Bridging Large Language Models and Action Languages for Complex Reasoning about Actions

T0 review · 3 major / 5 minor · reviewed 2026-08-10 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Pairing a large language model with the action language BC+ can solve complex action-reasoning puzzles that standalone LLMs miss, the paper claims, with only a few manual corrections to the generated logic program.

desk verdict Promising LLM-to-BC+ pipeline with a transparent appendix, but the headline comparison overstates the evidence: human corrections are often domain-knowledge injections, and the human-feedback baseline is a single anecdote. read the letter →

arxiv 2501.00830 v2 pith:IZGYRUTM submitted 2025-01-01 cs.CL cs.AI

Adam Ishay , Joohyung Lee This is my paper · ORCID

classification cs.CLcs.AI

keywords largelanguagemodelsactionlanguagesBC+automatedplanningsemanticparsingself-revisionelaborationtoleranceneuro-symbolicreasoning

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper tries to establish that current LLMs, though strong at natural language, cannot reliably do action reasoning that requires systematic search, but that this weakness can be bridged by having the LLM generate descriptions in the action language BC+ and letting a symbolic reasoner find plans. Using McCarthy's Missionaries-and-Cannibals elaborations and puzzle variations, it reports that the LLM+AL pipeline consistently reaches correct answers with only a few human corrections, while standalone ChatGPT-4, Claude 3 Opus, Gemini Ultra 1.0, o1-preview, and ChatGPT-4 with a code interpreter largely fail and do not improve with human feedback. If this holds, it matters because it identifies a practical division of labour: LLMs supply commonsense knowledge and semantic parsing, while declarative action languages supply the search and state-constraint enforcement that LLMs lack. It would also make action-language programming more accessible by automating much of the translation from English to formal rules.

What carries the argument

The load-bearing object is the action language BC+, a formal language whose declarative causal laws (causes, nonexecutable, impossible, increments, and decrements) describe transitions between states, with support for indirect effects, defaults, and additive fluents. The Cplus2ASP reasoner turns BC+ descriptions into answer-set programs and supplies the search and constraint solving. The pipeline's mechanism is a four-stage loop: the LLM generates a BC+ signature, extracts English knowledge, translates it into BC+ rules and a query, then self-revises using satisfiability checks and sample-query feedback from the reasoner, with a human correcting only the residual errors.

What would settle it

A controlled repair study would settle it: take the 30 problems, give an independent BC+ expert the same correction budget for LLM+AL's outputs, and give an equally skilled expert the same budget to repair ChatGPT-4, o1-preview, and ChatGPT-4+Code outputs, including fixing Python plans directly; if any baseline reaches LLM+AL's correctness at comparable effort, the paper's main claim fails. A quicker check is to repeat the reported 50-feedback ChatGPT-4 exchange on MCP elaboration #13 with a fixed protocol and see whether pointing out constraint violations ever converges to a correct plan.

Watch

Extended reading notes

Core claim

The paper's central claim is that an LLM can be made reliable at complex action reasoning by using it not as a final reasoner but as a generator of BC+ action-language descriptions, with a symbolic reasoner doing the search and a self-revision loop that feeds solver output back to the LLM. On McCarthy's elaboration-tolerant Missionaries-and-Cannibals benchmark and additional puzzle variations, LLM+AL automatically solves a substantial subset and reaches correct plans on the rest with an average of 3.1 (MCP) and 2.2 (other puzzles) manual corrections to the generated BC+ program. The paper contrasts this with ChatGPT-4, Claude 3 Opus, Gemini Ultra 1.0, o1-preview, and ChatGPT-4 with a code interpreter, which either produce wrong plans or cannot be repaired by human feedback.

Load-bearing premise

The central comparison assumes that the authors' handful of manual corrections to BC+ programs is genuinely less effort than the human feedback that standalone LLMs were given, even though the paper only documents one uncontrolled 50-iteration ChatGPT-4 exchange and does not count correction effort for the baselines.

Editorial extensions

If this is right

LLM+AL would solve 7 of 17 Missionaries-and-Cannibals elaborations outright, with an average of 3.1 manual corrections to the generated BC+ program for the rest, and on 13 additional puzzle and variation problems it solves 8 outright with an average of 2.2 corrections for the rest.
The self-revision stage would carry most of the repair burden: before it, only 22.3% of generated programs are executable and 16.6% produce correct answers, while after solver feedback executability rises to 86.7% and correct answers to 50%.
Standalone ChatGPT-4, Claude 3 Opus, Gemini Ultra 1.0, o1-preview, and ChatGPT-4 with a code interpreter would remain unable to produce consistently correct plans on these problems, and human feedback pointing out errors would not fix the direct-LLM failures.
Because BC+ is declarative, the pipeline would not need to encode a search strategy; the Cplus2ASP reasoner supplies search and constraint satisfaction, so correctness no longer depends on the LLM's ability to write correct search code.
If the pipeline's translation quality holds, action-language descriptions for new domains could be generated automatically rather than hand-authored by experts.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

A testable extension the paper does not run: apply the same pipeline to BC+ domains it mentions but does not benchmark, such as temporal prediction and postdiction, and measure whether correction counts stay low when the action vocabulary is larger.
A critical check the paper does not include: give independent annotators the same correction budget to repair ChatGPT-4+Code's Python plans directly on the same 30 problems, and compare accuracy at matched effort.
If the reported 50-iteration ChatGPT-4 failure is typical, the lesson generalizes beyond this benchmark: LLM reasoning without an external state-validating oracle cannot be repaired by pointing at mistakes, so methods that add a formal checker may be the only path to reliable correction.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Read this paper primarily for the pipeline. The idea of using an LLM to produce a BC+ signature, English knowledge, and rules, then letting the Cplus2ASP solver drive self-revision, is a real and useful step beyond LLM-to-PDDL or LLM-to-Python. The appendix is the best part: full BC+ programs, the exact prompts, and a detailed enumeration of 42 residual issues with concrete fixes. That transparency makes the work reproducible and is a credit to the authors.

The benchmark design is also reasonable. McCarthy's MCP elaborations are a good stress test for elaboration tolerance, and the directional result—LLM+AL solves more problems than direct LLM prompting, and the solver catches many issues automatically—is credible. The self-revision numbers (executability from 22% to 87%, correctness from 17% to 50%) are concrete and useful.

The soft spots are in the headline comparison. The claim that LLM+AL, with relatively minimal human corrections, beats standalone LLMs is weakened by three things. First, the correction counts are small in number but not in content: Appendix D shows several 'one correction' cases that inject a missing cannibal-outnumber constraint or a whole bail action. That is domain knowledge, not a typo fix. Second, the human-feedback baseline for standalone LLMs is a single undocumented 50-iteration exchange with ChatGPT-4 on one problem. That does not support the general statement that standalone LLMs fail to improve even with human feedback. Third, the paper is internally inconsistent: Section 4.1 says ChatGPT-4 solved only three MCP problems, while Table 1 lists six checkmarks. The authors need to fix that and add a protocol for author corrections, ideally with an independent annotator.

None of this kills the paper. The central pipeline contribution is real, and the ecosystem—code, prompts, detailed error logs—is exactly what a good systems paper should ship. But the evaluation should be qualified: the present evidence supports 'LLM+AL is a promising approach requiring human help,' not 'LLM+AL consistently outperforms LLMs with comparable human feedback.' A referee should ask for careful revision: more runs, a proper human-feedback condition for all baselines, and a clearer separation between automatic self-revision and author interventions.

This is for researchers working on neurosymbolic planning and action reasoning. It deserves a serious referee, and with revisions it could be a solid contribution. I would send it to review, with the caveat that the comparative claims need to be rewritten to match the evidence.

Referee Report

3 major / 5 minor

Summary. The paper introduces LLM+AL, a neuro-symbolic pipeline that uses an LLM (o1-preview) to generate programs in the action language BC+ from natural-language problem descriptions, then iteratively revises those programs using feedback from the Cplus2ASP solver. The method is evaluated on McCarthy's Missionaries-and-Cannibals elaborations and on several other puzzle domains, with comparison baselines including ChatGPT-4, Claude 3 Opus, Gemini Ultra 1.0, o1-preview, and ChatGPT-4+Code. The authors report that LLM+AL solves 7 of 17 MCP problems fully automatically and the remaining ones with an average of 3.1 human corrections, while standalone LLMs and LLM+Code perform worse and, the authors claim, do not improve even with human feedback. The paper also reports that its self-revision stage raises program executability from 22.3% to 86.7% and correct-answer rate from 16.6% to 50% over the 30 tested problems. The appendix provides the full prompts, concrete BC+ programs for the basic MCP, and a detailed enumeration of the 42 post-revision issues categorized into signature, rule, and query problems.

Significance. If the reported advantage is robust, the paper would make a meaningful contribution to neuro-symbolic reasoning about actions: it demonstrates that a declarative action language (BC+) combined with an LLM-based semantic parser and solver feedback can approach expert-level correctness on elaboration-tolerant planning puzzles, and it provides concrete evidence of the types of errors that remain. The authors deserve credit for shipping a reproducible artifact: the repository contains the baseline outputs, the exact prompts, and the BC+ programs, and the appendix's error catalog (Appendix D) names specific missing rules (e.g., the 'hungry' causation in MCP #17, the cannibal-outnumbering constraints in MCP #8, and the 'bail' rule in MCP #14) rather than vague summaries. Because correctness is verified by an external solver against known gold-standard plans, the evaluation is not circular. However, the headline comparison is currently weakened by the asymmetric treatment of human correction: LLM+AL receives author-administered corrections whose counts are reported, while the baselines' 'human feedback' condition is essentially anecdotal.

major comments (3)

[§4.2, Tables 1–2] The claim that standalone LLMs 'fail to improve even with human feedback' is not supported by commensurable evidence. The only human-feedback baseline is one anecdotal 50-iteration ChatGPT-4 exchange on MCP #13, with no protocol, no correction counts, and no human-feedback conditions for Claude, Gemini, o1-preview, or ChatGPT-4+Code. Meanwhile, LLM+AL receives author-administered corrections whose counts (3.1 and 2.2 per unsolved problem) are reported. As Appendix D shows, many of these corrections are substantive modeling decisions (e.g., MCP #17 needs a missing 'hungry' causation rule; MCP #8 needs the full cannibal-outnumbering constraints; MCP #14 needs a missing 'bail' rule), not trivial typo fixes. The paper should either provide a controlled comparison where baselines receive an equivalent amount of expert correction (with the same correction-effort metric), or explicitly narrow the claim to 'LLM+AL with a few manual corrections' without the comparative 'even with human feedback' statement.
[§4.1 vs. Table 1] There is an internal inconsistency in the reported ChatGPT-4 performance on the MCP benchmark. The text says 'ChatGPT-4 solves only three' MCP problems, but Table 1 shows six checkmarks for ChatGPT-4: MCP basic, #2, #10, #11, #14, and #19. This discrepancy affects the credibility of the headline comparison and the interpretation of 'solve.' The authors should clarify the counting criterion (e.g., whether optimality or manual re-checking is required) and ensure the prose and table agree.
[§4.1 and Tables 1–2] The experiments use a single run per problem per method, with no reporting of sampling variability for the stochastic LLM components. The abstract and conclusion use strong language such as 'consistently leads to correct answers,' and the self-revision statistics (22.3% to 86.7% executability, 16.6% to 50% correct) are presented as if they were deterministic. Because LLM outputs vary across runs, the observed 7/30 and 15/30 counts could change materially with different seeds or temperatures. The paper should report multiple runs (at least for LLM+AL and preferably for the strongest baselines such as o1-preview) or explicitly state that results are from a single run and weaken 'consistently' accordingly.

minor comments (5)

[Throughout] The rendering of model names as 'C HATGPT-4', 'C LAUDE 3 O PUS', and 'G EMINI ULTRA 1.0' appears in the abstract, introduction, and tables; this appears to be a spacing artifact and should be fixed.
[Appendix D.2] The 'missing necessary rules' entry for MCP #17 ('A rule which causes hungry to be true is required') is listed twice verbatim. One of the duplicates should be removed.
[§4.1 and Appendix D] The paper reports 'manual corrections' counts but never defines what counts as one correction (e.g., one edited rule vs. one logical issue). A brief definition would make the 3.1 and 2.2 averages interpretable.
[§4.2, footnote 5] The sentence about not guaranteeing non-existence of plans of arbitrary length points to 'Sec 6.6 of (Lee 2005)' with no appendix material; since the thesis is a dissertation, the reference should be expanded or the relevant technique summarized so the reader can verify the argument.
[Table 3] The column header 'Programs Issues' reads awkwardly and the table would benefit from clearer alignment between the subcategories (MD, Syn, Sem) and the 'Signature/Rules/Query' rows; this is purely a presentation matter.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: LLM+AL is an empirical pipeline validated against external benchmarks; the human-feedback asymmetry is an evaluation limitation, not a circular reduction.

full rationale

This paper does not derive its central claim from fitted parameters or from its own definitions. LLM+AL is an empirical pipeline: an LLM generates a BC+ signature, English knowledge, BC+ rules, and queries, and the Cplus2ASP reasoner (Babb and Lee 2013) is an independent tool with formal semantics. Final plans are checked against known puzzle ground truth, e.g., the McCarthy (1998) elaborations and optimal plan lengths reported in Tables 1 and 2, so correctness is not defined by the pipeline's own output. The manual corrections to generated BC+ programs (averaging 3.1 and 2.2 corrections) are debugging inputs, not fitted constants, and they do not make the solver's answer equivalent to the input by construction. The headline comparison is weakened by asymmetric human-feedback conditions: the 'standalone LLMs fail to improve even with human feedback' claim rests on a single anecdotal 50-iteration ChatGPT-4 exchange on MCP #13, with no comparable correction counts for other baselines. That is an evaluation-design limitation, not a circularity. Self-citations to BC+ (Babb and Lee 2015, 2020) and Cplus2ASP (Babb and Lee 2013) are not load-bearing for circularity because the reasoner's satisfiability results are externally checkable and the benchmarks are independent. No equation, definition, or fitted parameter is shown to reduce to its own input.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

No numeric free parameters are fitted. The method's performance depends on prompt design choices and on assumptions listed above, especially the typed input format and the comparability of human corrections, which are not independently measured.

assumptions (5)

standard math Answer set programming semantics and the Cplus2ASP compilation are sound for the causal laws used.
Section 2.2 presents BC+ as a high-level notation of answer set programs; the paper does not re-derive this.
domain assumption BC+ causal laws and the Cplus2ASP reasoner faithfully implement the intended transition systems for the benchmark domains.
Section 2.2 and Appendix A.6 treat Cplus2ASP output as ground truth for satisfiability, plans, and unsolvability.
domain assumption The typed problem descriptions, which enumerate sorts, objects, and action names, are a valid and sufficient input for both LLM+AL and baseline LLMs.
Section 3.1 and Appendix A.1 fix the input format; this explicit typing materially simplifies signature generation and is not guaranteed outside the benchmark.
domain assumption The benchmark elaborations are faithful, concreteness-completed versions of McCarthy's scenarios.
Section 4 and Appendix E say some elaborations are excluded as vague or probabilistic and that #17 was made more concrete; the scoring depends on these choices.
domain assumption o1-preview's generated commonsense knowledge and BC+ translations are sufficiently reliable that residual errors are correctable with a few manual fixes.
The entire pipeline rests on this empirical regularity; Section 4.2's issue counts document that errors remain in 15 of 30 final programs.

how reviews work

0 comments

Cite this review

Pith. "Pith review of LLM+AL: Bridging Large Language Models and Action Languages for Complex Reasoning about Actions." pith.science (2026). https://pith.science/paper/IZGYRUTM

@misc{pith2026250100830,
  author       = {Pith},
  title        = {Pith review of: LLM+AL: Bridging Large Language Models and Action Languages for Complex Reasoning about Actions},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/IZGYRUTM}},
  note         = {Machine review of arXiv:2501.00830}
}

read the original abstract

Large Language Models (LLMs) have made significant strides in various intelligent tasks but still struggle with complex action reasoning tasks that require systematic search. To address this limitation, we propose a method that bridges the natural language understanding capabilities of LLMs with the symbolic reasoning strengths of action languages. Our approach, termed "LLM+AL," leverages the LLM's strengths in semantic parsing and commonsense knowledge generation alongside the action language's proficiency in automated reasoning based on encoded knowledge. We compare LLM+AL against state-of-the-art LLMs, including ChatGPT-4, Claude 3 Opus, Gemini Ultra 1.0, and o1-preview, using benchmarks for complex reasoning about actions. Our findings indicate that, although all methods exhibit errors, LLM+AL, with relatively minimal human corrections, consistently leads to correct answers, whereas standalone LLMs fail to improve even with human feedback. LLM+AL also contributes to automated generation of action languages.

Figures

Figures reproduced from arXiv: 2501.00830 by the authors.

**Figure 1.** LLM+AL pipeline for this task. Domain-specific knowledge is directly tied to the given information about the problem, for instance, “Missionaries should not be outnumbered by cannibals, or they will be eaten." The full prompt for extracting knowledge is shown in Appendix B.2. The complete knowledge generated for MCP is shown in Appendix A.3. 3.4 Rules and Query Generation Further leveraging the capabilities of LLMs… view at source ↗

**Figure 2.** LLM+AL B.1 BC+ Signature Generation This prompt is used in the Signature Generation portion of Initial Program Generation, as shown in [PITH_FULL_IMAGE:figures/full_fig_p030_2.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

25 extracted references · 21 canonical work pages

[1]

impossible

In general, if some conjunction of fluents cannot be true, then we use "impossible" when writing the rules, but if instead we want to assert some constant is caused to be false, then we use the negation (~). For example, if it is impossible for an object to be on the table and under it, we might write "impossible onTable(object) & underTable(object).", bu...

work page
[2]

impossible F

"impossible F" can only be used with fluents and "&". Do not use attributes or action constants in laws of the form "impossible F". "nonexecutable" is about actions not being permissible if certain fluents hold and/or certain actions are performed

work page
[3]

Additive constants can only be updated in increment/decrement laws

work page
[4]

a causes G if H

In "a causes G if H", "G", recall G should be a fluent formula. Therefore, it should not directly contain action constants (including attributes). If one wants to set some constant to the value of an attribute, then the fluent formula G should contain a variable represnting the attribute, rather than the attribute itself. For example, if the attribute nex...

work page
[5]

Only use variables which are declared, if new variables are introduced, they must be declared

work page
[6]

default c=v if F

In shorthand laws "default c=v if F" and "default c=v if F after G", "c" cannot be an additive constant, since this is can update the value of them, but they should only be updated in increment/decrement laws

work page
[7]

always" shorthand abbreviations should not contain

"always" shorthand abbreviations should not contain "if", but only conjunctions ("&")

work page
[8]

In the case that a disjunction is used in the body of a rule, encapsulate it in parentheses, e.g., (loc(city1) | loc(city2))

work page

Show all 25 references

[9]

For example, do not use the following: nonexecutable move(C) if roadBlock(loc(C))

Do not nest constants in arguments of other constants. For example, do not use the following: nonexecutable move(C) if roadBlock(loc(C)). Instead, loc(C) should be set to a variable: nonexecutable move(C) if roadBlock(L) & L = loc(C)
[10]

Make sure that the query is exhaustive. For example, if the initial condition is that bus stop A has 10 people, and the goal condition is that the bus stop B has 10 people, it may need to be specified that bus stop B has 0 people in the initial condition, or the BC + solver ca...
[11]

If new constans are used, then they must be added in the declaration

Make sure to only use constants which are declared in the constant declaration. If new constans are used, then they must be added in the declaration
[12]

capacity(vehicle)

Make sure when writing rules, that variables representing constants are of the correct sort, i.e., the sort of the variable is the same as the sort of the value of the constant it is representing. For example, if there is a constant "capacity(vehicle)" which is of type "inerti...
[13]

inertialFluent

Don’t use simple, or rigid fluents in the constant declaration. Use "inertialFluent" instead
[14]

country(location) :: country

Don’t use non-specified fluents. For example, there should not be constant declarations like "country(location) :: country", since this will be recognized as a rigid fluent
[15]

always F

Keep in mind that "always F" should be used for conditions which should be true for every transition and shout not be used to express conditions for a state. For example, consider a domain about trading coins that has the action constant numExchanged( coin), which is an attrib...
[16]

They must be set to variables, and the variables must be used as the operands

Attributes and additive actions should not occur in the operands of arithmetics such as addition, subtraction, multiplication, floor division, or modulus operators. They must be set to variables, and the variables must be used as the operands. [INSTRUCTIONS] Consider the probl...
[22]

[ CHANGED]

[FEEDBACK OUTLINE] Based on the feedback, if any of the following segments are incorrect, then mark them with "[ CHANGED]", and revise them: - PROGRAM - MAIN QUERY - SAMPLE QUERIES Otherwise, if a segment is correct, mark it with "[UNCHANGED]", and simply copy their contents
[23]

In some cases, the sample queries themselves may be wrong (e.g., a syntax error), and can be re-written

[SAMPLE QUERY GUIDANCE] Keep in mind, the outputs from running the sample queries is to help check that the program is working properly. In some cases, the sample queries themselves may be wrong (e.g., a syntax error), and can be re-written. The sample queries marked (satisfia...
[24]

Main query and output

[MAIN QUERY OUTPUT] IMPORTANT: Check that each action in the final plan of the main query makes sense given the state before it, and that the resulting state correctly follows. If something doesn’t align with the common sense relative to the problem description, then update th...
[25]

int” needs objects instantiated from 0 to 8 (written “0..8

[FORMAT] The format should be like the following, encapsulated in 3 backticks: ‘‘‘% PROGRAM CHANGED? [CHANGED/UNCHANGED] % BC+ signature <Enter BC+ signature> % Generated constraints <Enter BC+ rules/constraints> % MAIN QUERY CHANGED? [CHANGED/UNCHANGED] <Enter the main query>...

1998
[318]

Chen, J.; Chen, L.; Huang, H.; and Zhou, T

PMLR. Chen, J.; Chen, L.; Huang, H.; and Zhou, T. 2023a. When do you need chain-of-thought prompting for chatgpt? arXiv preprint arXiv:2304.03262. Chen, W.; Ma, X.; Wang, X.; and Cohen, W. W. 2023b. Pro- gram of Thoughts Prompting: Disentangling Computation from Reasoning for ...

2006 arXiv
[2019]

Frontiers of Information Tech- nology & Electronic Engineering, 20: 363–373

Task planning in robotics: an empirical comparison of pddl-and asp-based systems. Frontiers of Information Tech- nology & Electronic Engineering, 20: 363–373. Kamoi, R.; Zhang, Y .; Zhang, N.; Han, J.; and Zhang, R
[2021]

o1-preview

Improving coherence and consistency in neural se- quence models with dual-system, neuro-symbolic reason- ing. Advances in Neural Information Processing Systems , 34: 25192–25204. Olausson, T.; Gu, A.; Lipkin, B.; Zhang, C.; Solar-Lezama, A.; Tenenbaum, J.; and Levy, R. 2023. L...

2023 arXiv
[2023]

In Conference on robot learning, 287–

Do as i can, not as i say: Grounding language in robotic affordances. In Conference on robot learning, 287–
[2024]

Kim, G.; Baldi, P.; and McAleer, S

When Can LLMs Actually Correct Their Own Mis- takes? A Critical Survey of Self-Correction of LLMs.Trans- actions of the Association for Computational Linguistics , 12: 1417–1440. Kim, G.; Baldi, P.; and McAleer, S. 2024. Language models can solve computer tasks. Advances in Ne...

2024 arXiv

Pith tools

Reviewed August 10, 2026 · model on record in the stance chip above.

[1] [1]

impossible

In general, if some conjunction of fluents cannot be true, then we use "impossible" when writing the rules, but if instead we want to assert some constant is caused to be false, then we use the negation (~). For example, if it is impossible for an object to be on the table and under it, we might write "impossible onTable(object) & underTable(object).", bu...

work page

[2] [2]

impossible F

"impossible F" can only be used with fluents and "&". Do not use attributes or action constants in laws of the form "impossible F". "nonexecutable" is about actions not being permissible if certain fluents hold and/or certain actions are performed

work page

[3] [3]

Additive constants can only be updated in increment/decrement laws

work page

[4] [4]

a causes G if H

In "a causes G if H", "G", recall G should be a fluent formula. Therefore, it should not directly contain action constants (including attributes). If one wants to set some constant to the value of an attribute, then the fluent formula G should contain a variable represnting the attribute, rather than the attribute itself. For example, if the attribute nex...

work page

[5] [5]

Only use variables which are declared, if new variables are introduced, they must be declared

work page

[6] [6]

default c=v if F

In shorthand laws "default c=v if F" and "default c=v if F after G", "c" cannot be an additive constant, since this is can update the value of them, but they should only be updated in increment/decrement laws

work page

[7] [7]

always" shorthand abbreviations should not contain

"always" shorthand abbreviations should not contain "if", but only conjunctions ("&")

work page

[8] [8]

In the case that a disjunction is used in the body of a rule, encapsulate it in parentheses, e.g., (loc(city1) | loc(city2))

work page