Refining Gelfond Rationality Principle: Towards More Comprehensive Foundational Principles for Answer Set Semantics

Thomas Eiter; Yi-Dong Shen

arxiv: 2507.01833 · v2 · submitted 2025-07-02 · 💻 cs.AI

Refining Gelfond Rationality Principle: Towards More Comprehensive Foundational Principles for Answer Set Semantics

Yi-Dong Shen , Thomas Eiter This is my paper

Pith reviewed 2026-05-19 06:25 UTC · model grok-4.3

classification 💻 cs.AI

keywords answer set programmingnon-monotonic logicGelfond rationality principlewell-supportednessnegation by defaultepistemic negationworld views

0 comments

The pith

Answer set semantics need not require the minimal model property, constraint monotonicity and foundedness in every case.

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

The paper examines whether three standard conditions on answer sets—the minimal model property, constraint monotonicity, and foundedness—must always be enforced. It presents programs where these conditions rule out sets that intuition suggests should be included. In response, the authors refine Gelfond’s rationality principle into three replacement conditions: well-supportedness, minimality with respect to negation by default, and minimality with respect to epistemic negation. Well-supportedness ensures every answer set can be built from if-then rules that obey a level mapping and therefore contains no circular justification. The two minimality conditions ensure that knowledge is minimized both inside individual answer sets and across collections of answer sets called world views. The paper then extends the notion of well-supportedness to cover both answer sets and world views, defines new semantics that obey the refined principles, and uses the principles to evaluate existing semantics.

Core claim

By replacing Gelfond’s original rationality principle with the three conditions of well-supportedness, minimality w.r.t. negation by default, and minimality w.r.t. epistemic negation, answer-set semantics can be formulated so that every answer set is free of circular justification, knowledge is minimized at both the level of answer sets and the level of world views, and programs are allowed to possess answer sets that the stricter traditional conditions would have excluded.

What carries the argument

The refined Gelfond answer set (GAS) principles, consisting of well-supportedness (answer sets constructible from if-then rules under a level mapping) together with minimality w.r.t. negation by default and minimality w.r.t. epistemic negation.

If this is right

New answer-set semantics can be defined directly from the refined principles without invoking the three stronger conditions.
Well-supportedness can be extended uniformly to both answer sets and world views.
Existing answer-set semantics can be classified and compared by checking how well they satisfy the refined principles.
The computational complexity of the new semantics follows from the definitions based on the three principles.

Where Pith is reading between the lines

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

Programs that previously lacked answer sets under strict minimality may now receive stable solutions under the refined principles.
The same refinement pattern could be applied to other non-monotonic formalisms that rely on similar rationality assumptions.
Implementations could offer the refined semantics as an optional mode when the traditional conditions produce empty or unexpected results.

Load-bearing premise

The minimal model property, constraint monotonicity and foundedness are sometimes too strong and exclude answer sets that should be accepted.

What would settle it

A concrete logic program together with an answer set that satisfies the three refined conditions yet contains a circular justification or fails to minimize knowledge at either the answer-set or world-view level.

read the original abstract

Non-monotonic logic programming is the basis for a declarative problem solving paradigm known as answer set programming (ASP). Departing from the seminal definition by Gelfond and Lifschitz in 1988 for simple normal logic programs, various answer set semantics have been proposed for extensions. We consider two important questions: (1) Should the minimal model property, constraint monotonicity and foundedness as defined in the literature be mandatory conditions for an answer set semantics in general? (2) If not, what other properties could be considered as general principles for answer set semantics? We address the two questions. First, it seems that the three aforementioned conditions may sometimes be too strong, and we illustrate with examples that enforcing them may exclude expected answer sets. Second, we evolve the Gelfond answer set (GAS) principles for answer set construction by refining the Gelfond's rationality principle to well-supportedness, minimality w.r.t. negation by default and minimality w.r.t. epistemic negation. The principle of well-supportedness guarantees that every answer set is constructible from if-then rules obeying a level mapping and is thus free of circular justification, while the two minimality principles ensure that the formalism minimizes knowledge both at the level of answer sets and of world views. Third, to embody the refined GAS principles, we extend the notion of well-supportedness substantially to answer sets and world views, respectively. Fourth, we define new answer set semantics in terms of the refined GAS principles. Fifth, we use the refined GAS principles as an alternative baseline to intuitively assess the existing answer set semantics. Finally, we analyze the computational complexity.

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.

Desk Editor's Note private letter to a colleague

This refines Gelfond's rationality principle into well-supportedness plus separate minimality for default and epistemic negation, then extends it to world views, but the level-mapping argument for epistemic cases in complex rules looks incomplete.

read the letter

The paper's core move is to replace the original Gelfond rationality principle with three pieces: well-supportedness (every answer set built from if-then rules under a level mapping), minimality with respect to default negation, and minimality with respect to epistemic negation. They then lift well-supportedness to world views and use the whole package both to define new semantics and to re-evaluate existing ones. The examples showing that strict minimal-model, constraint-monotonicity, and foundedness conditions can exclude intuitively expected answer sets are the clearest contribution; they give concrete cases where those older requirements bite too hard. The complexity analysis is also new ground for the refined principles. What the work does cleanly is keep the discussion inside the existing literature on GAS principles and avoid inventing new primitives out of thin air. The split minimality conditions are a reasonable way to separate concerns that were previously bundled together. The soft spot is the extension of well-supportedness to world views when epistemic negation appears inside disjunctive rules or aggregates. The manuscript states the extension but does not supply an explicit inductive construction or a counter-example sweep that confirms the level mapping stays well-founded and non-circular in those cases. Without that step the claim that the new semantics are free of circular justification rests on an unstated assumption about how the mapping behaves under epistemic negation. This is a fixable gap rather than a fatal one, but it is load-bearing for the main technical claim. The paper is written for researchers who care about the foundations of answer-set programming and non-monotonic reasoning. Anyone already working with Gelfond-Lifschitz style semantics or comparing multiple ASP variants will find the examples and the alternative baseline useful. It is coherent on its own terms and engages the literature honestly, so it should go to peer review. Ask the authors for the missing inductive argument on the level mappings before acceptance.

Referee Report

2 major / 2 minor

Summary. The manuscript questions whether the minimal model property, constraint monotonicity, and foundedness must be mandatory for answer set semantics in general. It illustrates cases where these may exclude expected answer sets, then refines the Gelfond answer set (GAS) principles by replacing the rationality principle with well-supportedness together with minimality w.r.t. negation by default and minimality w.r.t. epistemic negation. The work extends well-supportedness to answer sets and world views, defines new semantics embodying the refined principles, uses those principles as a baseline to assess existing semantics, and analyzes computational complexity.

Significance. If the extension of well-supportedness to world views is shown to preserve well-founded level mappings without circularity, the refined principles could supply a more flexible yet still principled foundation for answer set semantics, accommodating intuitive models that stricter minimality conditions exclude. The use of the refined GAS principles as an assessment baseline and the complexity analysis are constructive contributions that build directly on the cited Gelfond-Lifschitz and prior GAS literature.

major comments (2)

[Extension of well-supportedness to world views] The central extension of well-supportedness to world views (described after the refinement of the GAS principles) defines the notion but supplies neither an explicit inductive argument nor a counter-example verification that level mappings remain well-founded when epistemic negation occurs inside disjunctive rules or aggregates. This is load-bearing for the claim that every world view is constructible from if-then rules without circular justification.
[Illustrative examples] The illustrative examples used to show that minimal model property, constraint monotonicity and foundedness can exclude expected answer sets (early in the manuscript) are not cross-checked against the new minimality conditions; without this verification it is unclear whether the examples are actually admitted by the proposed semantics or whether the refinement inadvertently reintroduces similar exclusions.

minor comments (2)

[Notation] Notation for epistemic negation and level mappings should be introduced once and used uniformly; scattered re-definitions make the extension section harder to follow.
[Assessment of existing semantics] A short table summarizing which existing semantics satisfy each of the three refined principles would improve readability of the assessment section.

Simulated Author's Rebuttal

2 responses · 0 unresolved

Thank you for the referee's thoughtful and constructive comments on our manuscript. We have carefully considered each major comment and provide our responses below. We agree that additional details and verifications will enhance the clarity and rigor of our work on refining the Gelfond rationality principle.

read point-by-point responses

Referee: The central extension of well-supportedness to world views (described after the refinement of the GAS principles) defines the notion but supplies neither an explicit inductive argument nor a counter-example verification that level mappings remain well-founded when epistemic negation occurs inside disjunctive rules or aggregates. This is load-bearing for the claim that every world view is constructible from if-then rules without circular justification.

Authors: We thank the referee for highlighting this important aspect. Upon review, the manuscript presents the definition of well-supportedness for world views but indeed lacks an explicit inductive argument or verification via counter-examples for scenarios where epistemic negation appears in disjunctive rules or aggregates. We will revise the manuscript to include a formal inductive proof that establishes the well-foundedness of the level mappings in these cases, thereby supporting the claim that world views are constructed without circular justification. revision: yes
Referee: The illustrative examples used to show that minimal model property, constraint monotonicity and foundedness can exclude expected answer sets (early in the manuscript) are not cross-checked against the new minimality conditions; without this verification it is unclear whether the examples are actually admitted by the proposed semantics or whether the refinement inadvertently reintroduces similar exclusions.

Authors: We agree with the observation. The illustrative examples in the early sections demonstrate potential exclusions under traditional properties but were not explicitly re-evaluated under the new minimality conditions. In the revised manuscript, we will provide a detailed cross-check for each example to verify that they satisfy the refined principles and are thus admitted by the proposed semantics. revision: yes

Circularity Check

0 steps flagged

No significant circularity in refinement of Gelfond rationality principles

full rationale

The paper questions whether minimal model property, constraint monotonicity and foundedness must be mandatory, illustrates counter-examples, then refines the Gelfond rationality principle into well-supportedness (every answer set constructible from if-then rules under a level mapping), minimality w.r.t. default negation and minimality w.r.t. epistemic negation. These notions are drawn from prior literature on level mappings and foundedness rather than being fitted to the paper's own data or equations. New semantics are defined directly from the refined principles, and the principles are applied as a baseline to evaluate existing semantics. Self-citations to Gelfond-Lifschitz 1988 and prior GAS work exist but are not load-bearing in a way that reduces the central claims to unverified self-references; the manuscript supplies independent examples, extensions to world views, and complexity results. No derivation step equates a result to its inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper rests on standard background assumptions of non-monotonic logic programming and the original Gelfond-Lifschitz stable-model definition; no new free parameters or invented entities are introduced in the abstract.

axioms (1)

standard math Standard properties of logic programs and negation as failure from the Gelfond-Lifschitz 1988 definition
Invoked when discussing extensions of answer set semantics

pith-pipeline@v0.9.0 · 5831 in / 1102 out tokens · 39458 ms · 2026-05-19T06:25:57.103549+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

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

IndisputableMonolith/Foundation/ArithmeticFromLogic.lean embed_strictMono_of_one_lt, LogicNat.wellFoundedLT echoes

?

echoes
ECHOES: this paper passage has the same mathematical shape or conceptual pattern as the Recognition theorem, but is not a direct formal dependency.

We extend the notion of well-supportedness substantially to answer sets and world views... there exists a strict well-founded partial order ≺ ... q ≺ p for every q ∈ S (Definition 7, 10, 13, 15).
IndisputableMonolith/Cost/FunctionalEquation.lean Jcost_pos_of_ne_one, washburn_uniqueness_aczel echoes

?

echoes
ECHOES: this paper passage has the same mathematical shape or conceptual pattern as the Recognition theorem, but is not a direct formal dependency.

minimality of answer sets w.r.t. negation by default... maximal set of ground atoms being false... (RP1)

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

16 extracted references · 16 canonical work pages

[1]

Amendola, G., Cuteri, B., Ricca, F., & Truszczynski, M. (2022). Solving problems in the poly- nomial hierarchy with ASP(Q). In Gottlob, G., Inclezan, D., & Maratea, M. (Eds.), Logic Programming and Nonmonotonic Reasoning - 16th International Conference, LPNMR 2022, Genova, Italy, September 5-9, 2022, Proceedings , Vol. 13416 of Lecture Notes in Computer S...

work page 2022
[2]

, pp. 119–131. Ferraris, P., Lee, J., & Lifschitz, V. (2011). Stable models and circumscription. Artif. Intell. , 175(1), 236–263. Ferraris, P., & Lifschitz, V. (2005). Mathematical foundations of answer set programming. In We Will Show Them! Essays in Honour of Dov Gabbay, Volume One , pp. 615–664. Fierens, D., den Broeck, G. V., Renkens, J., Shterionov,...

work page 2011
[3]

, pp. 260–265. Gelfond, M. (1991). Strong introspection. In Proc. 9th National Conference on Artificial Intelli- gence (AAAI

work page 1991
[4]

, pp. 386–391. Gelfond, M. (2008). Answer sets. In van Harmelen, F., Lifschitz, V., & Porter, B. (Eds.), Handbook of Knowledge Representation , Foundations of Artificial Intelligence, chap. 7, pp. 285–316. Elsevier. Gelfond, M., & Kahl, Y. (2014). Knowledge Representation, Reasoning, and the Design of Intelli- gent Agents. Cambridge University Press. 57 G...

work page 2008
[5]

1070–1080

, pp. 1070–1080. Gelfond, M., & Lifschitz, V. (1991). Classical negation in logic programs and disjunctive databases. New Generation Computing , 9, 365–385. Hirate, T., Banbara, M., Inoue, K., Lu, X., Nabeshima, H., Schaub, T., Soh, T., & Tamura, N. (2023). Hamiltonian cycle reconfiguration with answer set programming. In Logics in Arti- ficial Intelligen...

work page 1991
[6]

, pp. 1–17. Leone, N., Pfeifer, G., Faber, W., Eiter, T., Gottlob, G., Perri, S., & Scarcello, F. (2006). The dlv system for knowledge repsentation and reasoning. ACM Trans. Comput. Logic , 7(3), 499–562. Leone, N., Rullo, P., & Scarcello, F. (1997). Disjunctive stable models: Unfounded sets, fixpoint semantics, and computation. Information and Compututat...

work page 2006
[7]

, pp. 23–37. Lukasiewicz, T. (2010). A novel combination of answer set programming with description logics for the semantic web. IEEE TKDE, 22(11), 1577–1592. Marek, V. W., & Truszczy´ nski, M. (1999). Stable models and an alternative logic program- ming paradigm. In The Logic Programming Paradigm: A 25-Year Perspective, pp. 375–398. Springer. Minker, J. ...

work page arXiv 2010
[8]

, pp. 113–126. Su, E. I., del Cerro, L. F., & Herzig, A. (2020). Autoepistemic equilibrium logic and epistemic specifications. Artif. Intell., 282, 103–249. Truszczy´ nski, M. (2010). Reducts of propositional theories, satisfiability relations, and generaliza- tions of semantics of logic programs. Artif. Intell., 174(16-17), 1285–1306. Wagner, K. W. (1990...

work page 2020
[9]

Deciding whether a model I of a simple epistemic-free normal program Π is well- supported in Π is P-complete. Proof. By Theorem 2, we need to check whether lfp(TΠ(∅, ¬I −)) = I holds. Since Π is simple, evaluating each stage T i Π(∅, ¬I −) of the fixpoint iteration for lfp(TΠ′(∅, ¬I −)) is feasible in poly- nomial time, and thus computing lfp(TΠ′(∅, ¬I −)...

work page 2007
[10]

Morevoer, PNP ∥ -hardness holds if D(A) is a Boolean formula and Π is simple

Deciding whether an epistemic model A of an epistemic normal program Π is well- supported in Π is PNP ∥ -complete under implicit representation. Morevoer, PNP ∥ -hardness holds if D(A) is a Boolean formula and Π is simple. Proof. By Lemma 5, we can compute Π A in polynomial time with one round of NP oracle calls. Exploiting Theorem 9, we can then consult ...

work page 1990
[11]

Given a normal epistemic program Π with atomic heads, deciding whether Π has some rational world view is Σp 3-complete. Proof. Membership in Σp 3 follows from Lemma 8.(i) and Σ p 2 / Πp 2-completeness of brave / cautious inference for normal epistemic-free programs (row 1 of Table 2). 71 We show Σp 3-hardness by a reduction from evaluating QBFs of the for...

work page 2016
[12]

The Σp 4-hardness holds even if F is an atom

Given a normal epistemic program Π with atomic heads and a formula F , deciding whether F is true in some rational world view of Π is Σp 4-complete. The Σp 4-hardness holds even if F is an atom. Proof. Membership in Σp 4 follows from Lemma 8.(ii) and Σp 2 / Πp 2- completeness of brave / cautious inference for normal epistemic-free programs (row 1 of Table...

work page 2016
[13]

Given a simple disjunctive epistemic program Π, deciding whether Π has some rational world view is Σp 3-complete. Proof. Membership in Σp 3 follows from Lemma 8.(i) and Σp 2 / Πp 2- completeness of brave / cautious inference for simple disjunctive epistemic-free programs (row 1 of Table 2). The Σp 3-hardness is shown by a minor adaptation of the proof of ...

work page 2016
[14]

which showed Σ p 4-hardness of deciding whether an atom F is true in some EFLP world view of a normal epistemic program. The program Π 1 was constructed from the program 73 Π in the proof of Theorem 5 of (Shen & Eiter, 2016), which has an EFLP world view iff a given QBF ∃X∀Y ∃Z.ϕ(X, Y, Z) (18) evaluates to true, as follows: Π1 = {H ← B∗ ∧ A | H ← B ∈ Π} ∪...

work page 2016
[15]

Given an epistemic program Π, deciding whether Π has some rational world view is Σp 4-complete, and Σp 4-hardness holds even for atomic heads. Proof. Membership in Σp 4 follows from Lemma 8.(i) and Σp 3- / Πp 3- completeness of brave / cautious inference for disjunctive epistemic-free programs. The Σp 4-hardness is shown by extending the encoding of MINQA...

work page 2019
[16]

Given an epistemic program Π and a formula F , deciding whether F is true in some rational world view of Π is Σp 5-complete, and Σp 5-hardness holds even for atomic heads and F being an atom. Proof. (Sketch) Membership in Σ p 5 follows from Lemma 8.(ii) and Σ p 3 / Πp 3- completeness of brave / cautious inference for disjunctive epistemic-free programs (r...

work page 2016

[1] [1]

Amendola, G., Cuteri, B., Ricca, F., & Truszczynski, M. (2022). Solving problems in the poly- nomial hierarchy with ASP(Q). In Gottlob, G., Inclezan, D., & Maratea, M. (Eds.), Logic Programming and Nonmonotonic Reasoning - 16th International Conference, LPNMR 2022, Genova, Italy, September 5-9, 2022, Proceedings , Vol. 13416 of Lecture Notes in Computer S...

work page 2022

[2] [2]

, pp. 119–131. Ferraris, P., Lee, J., & Lifschitz, V. (2011). Stable models and circumscription. Artif. Intell. , 175(1), 236–263. Ferraris, P., & Lifschitz, V. (2005). Mathematical foundations of answer set programming. In We Will Show Them! Essays in Honour of Dov Gabbay, Volume One , pp. 615–664. Fierens, D., den Broeck, G. V., Renkens, J., Shterionov,...

work page 2011

[3] [3]

, pp. 260–265. Gelfond, M. (1991). Strong introspection. In Proc. 9th National Conference on Artificial Intelli- gence (AAAI

work page 1991

[4] [4]

, pp. 386–391. Gelfond, M. (2008). Answer sets. In van Harmelen, F., Lifschitz, V., & Porter, B. (Eds.), Handbook of Knowledge Representation , Foundations of Artificial Intelligence, chap. 7, pp. 285–316. Elsevier. Gelfond, M., & Kahl, Y. (2014). Knowledge Representation, Reasoning, and the Design of Intelli- gent Agents. Cambridge University Press. 57 G...

work page 2008

[5] [5]

1070–1080

, pp. 1070–1080. Gelfond, M., & Lifschitz, V. (1991). Classical negation in logic programs and disjunctive databases. New Generation Computing , 9, 365–385. Hirate, T., Banbara, M., Inoue, K., Lu, X., Nabeshima, H., Schaub, T., Soh, T., & Tamura, N. (2023). Hamiltonian cycle reconfiguration with answer set programming. In Logics in Arti- ficial Intelligen...

work page 1991

[6] [6]

, pp. 1–17. Leone, N., Pfeifer, G., Faber, W., Eiter, T., Gottlob, G., Perri, S., & Scarcello, F. (2006). The dlv system for knowledge repsentation and reasoning. ACM Trans. Comput. Logic , 7(3), 499–562. Leone, N., Rullo, P., & Scarcello, F. (1997). Disjunctive stable models: Unfounded sets, fixpoint semantics, and computation. Information and Compututat...

work page 2006

[7] [7]

, pp. 23–37. Lukasiewicz, T. (2010). A novel combination of answer set programming with description logics for the semantic web. IEEE TKDE, 22(11), 1577–1592. Marek, V. W., & Truszczy´ nski, M. (1999). Stable models and an alternative logic program- ming paradigm. In The Logic Programming Paradigm: A 25-Year Perspective, pp. 375–398. Springer. Minker, J. ...

work page arXiv 2010

[8] [8]

, pp. 113–126. Su, E. I., del Cerro, L. F., & Herzig, A. (2020). Autoepistemic equilibrium logic and epistemic specifications. Artif. Intell., 282, 103–249. Truszczy´ nski, M. (2010). Reducts of propositional theories, satisfiability relations, and generaliza- tions of semantics of logic programs. Artif. Intell., 174(16-17), 1285–1306. Wagner, K. W. (1990...

work page 2020

[9] [9]

Deciding whether a model I of a simple epistemic-free normal program Π is well- supported in Π is P-complete. Proof. By Theorem 2, we need to check whether lfp(TΠ(∅, ¬I −)) = I holds. Since Π is simple, evaluating each stage T i Π(∅, ¬I −) of the fixpoint iteration for lfp(TΠ′(∅, ¬I −)) is feasible in poly- nomial time, and thus computing lfp(TΠ′(∅, ¬I −)...

work page 2007

[10] [10]

Morevoer, PNP ∥ -hardness holds if D(A) is a Boolean formula and Π is simple

Deciding whether an epistemic model A of an epistemic normal program Π is well- supported in Π is PNP ∥ -complete under implicit representation. Morevoer, PNP ∥ -hardness holds if D(A) is a Boolean formula and Π is simple. Proof. By Lemma 5, we can compute Π A in polynomial time with one round of NP oracle calls. Exploiting Theorem 9, we can then consult ...

work page 1990

[11] [11]

Given a normal epistemic program Π with atomic heads, deciding whether Π has some rational world view is Σp 3-complete. Proof. Membership in Σp 3 follows from Lemma 8.(i) and Σ p 2 / Πp 2-completeness of brave / cautious inference for normal epistemic-free programs (row 1 of Table 2). 71 We show Σp 3-hardness by a reduction from evaluating QBFs of the for...

work page 2016

[12] [12]

The Σp 4-hardness holds even if F is an atom

Given a normal epistemic program Π with atomic heads and a formula F , deciding whether F is true in some rational world view of Π is Σp 4-complete. The Σp 4-hardness holds even if F is an atom. Proof. Membership in Σp 4 follows from Lemma 8.(ii) and Σp 2 / Πp 2- completeness of brave / cautious inference for normal epistemic-free programs (row 1 of Table...

work page 2016

[13] [13]

Given a simple disjunctive epistemic program Π, deciding whether Π has some rational world view is Σp 3-complete. Proof. Membership in Σp 3 follows from Lemma 8.(i) and Σp 2 / Πp 2- completeness of brave / cautious inference for simple disjunctive epistemic-free programs (row 1 of Table 2). The Σp 3-hardness is shown by a minor adaptation of the proof of ...

work page 2016

[14] [14]

which showed Σ p 4-hardness of deciding whether an atom F is true in some EFLP world view of a normal epistemic program. The program Π 1 was constructed from the program 73 Π in the proof of Theorem 5 of (Shen & Eiter, 2016), which has an EFLP world view iff a given QBF ∃X∀Y ∃Z.ϕ(X, Y, Z) (18) evaluates to true, as follows: Π1 = {H ← B∗ ∧ A | H ← B ∈ Π} ∪...

work page 2016

[15] [15]

Given an epistemic program Π, deciding whether Π has some rational world view is Σp 4-complete, and Σp 4-hardness holds even for atomic heads. Proof. Membership in Σp 4 follows from Lemma 8.(i) and Σp 3- / Πp 3- completeness of brave / cautious inference for disjunctive epistemic-free programs. The Σp 4-hardness is shown by extending the encoding of MINQA...

work page 2019

[16] [16]

Given an epistemic program Π and a formula F , deciding whether F is true in some rational world view of Π is Σp 5-complete, and Σp 5-hardness holds even for atomic heads and F being an atom. Proof. (Sketch) Membership in Σ p 5 follows from Lemma 8.(ii) and Σ p 3 / Πp 3- completeness of brave / cautious inference for disjunctive epistemic-free programs (r...

work page 2016