pith. sign in

arxiv: 2605.19819 · v1 · pith:LQAFIN4Ynew · submitted 2026-05-19 · 💻 cs.LO

Satisfiability for Knowing How over Linear Plans is NP-complete

Carlos Areces , Pablo Barcel\'o , Valentin Cassano , Pablo F. Castro , St\'ephane Demri , Raul Fervari This is my paper

Pith reviewed 2026-05-20 01:35 UTC · model grok-4.3

classification 💻 cs.LO
keywords knowing-howmodal logicsatisfiabilityNP-completelinear plansS5epistemic logicknowledge representation
0
0 comments X

The pith

Satisfiability for knowing-how logic over linear plans is NP-complete.

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

The paper establishes that satisfiability of formulas in the knowing-how modal logic is NP-complete when evaluated over linear plans. This tightens earlier upper and lower bounds on the decision problem. A sympathetic reader cares because the logic directly models an agent's capacity to reach goals via executable plans, which underpins reasoning about practical knowledge in AI systems. The authors obtain the result by exhibiting a satisfiability-preserving translation from knowing-how assertions into the modal logic S5.

Core claim

We study the satisfiability problem for a modal logic expressing knowing-how assertions, which captures an agent's ability to achieve a given goal under the standard semantics based on linear plans. Our main result shows that satisfiability of knowing-how formulas is NP-complete, improving previously known complexity bounds. The proof proceeds via a translation into modal logic S5, an instrumental tool for addressing a variety of problems in knowledge representation.

What carries the argument

A satisfiability-preserving translation from knowing-how formulas into S5 modal logic formulas that reduces the decision problem to a known NP-complete task.

If this is right

  • Satisfiability of knowing-how formulas lies in NP and is therefore decidable by nondeterministic polynomial-time procedures.
  • The problem is NP-hard, inheriting hardness from propositional satisfiability via the translation.
  • Practical verification of knowing-how statements becomes feasible for bounded-size formulas by reduction to existing S5 solvers.

Where Pith is reading between the lines

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

  • The same reduction technique may transfer to other plan-based epistemic operators and yield matching complexity results.
  • Efficient SAT encodings derived from the S5 translation could support automated checking of agent abilities in planning domains.
  • Relaxing the linear-plan restriction to allow branching or looping plans might raise the complexity above NP.

Load-bearing premise

The result assumes the standard semantics for knowing-how based on linear plans and that the translation into S5 modal logic correctly preserves satisfiability.

What would settle it

A concrete polynomial-time algorithm for satisfiability of knowing-how formulas, or a specific formula for which the S5 translation fails to preserve satisfiability, would refute the NP-completeness claim.

read the original abstract

We study the satisfiability problem for a modal logic expressing knowing-how assertions, which captures an agent's ability to achieve a given goal under the standard semantics based on linear plans. Our main result shows that satisfiability of knowing-how formulas is NP-complete, improving previously known complexity bounds. The proof proceeds via a translation into modal logic S5, an instrumental tool for addressing a variety of problems in knowledge representation.

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

1 major / 2 minor

Summary. The manuscript examines the satisfiability problem for a modal logic of knowing-how assertions interpreted over linear plans. The central result establishes that this problem is NP-complete by means of a satisfiability-preserving translation into the modal logic S5, whose satisfiability problem is already known to be NP-complete.

Significance. If the translation is shown to be faithful in both directions while correctly capturing the linear-plans restriction, the result tightens previously known complexity bounds for knowing-how logics and illustrates a useful reduction technique connecting epistemic planning to classical modal logic. The approach is technically economical and leverages an independently studied logic.

major comments (1)
  1. [§4.1–4.3] §4.1–4.3 (the translation and its correctness proof): the argument that the mapping preserves satisfiability in both directions must explicitly address how the linearity constraint on plans is enforced inside S5 models; if S5 equivalence classes can encode branching or non-linear executions not permitted by the original semantics, then membership in NP via the S5 reduction or the hardness direction would fail to follow.
minor comments (2)
  1. [Definition 2.3] Definition 2.3: the notation for plan execution could be accompanied by a small concrete example showing how a linear plan satisfies a knowing-how formula.
  2. [Introduction] The abstract and introduction cite prior complexity results but do not explicitly state the exact previous bound being improved; adding a sentence with the reference would clarify the contribution.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading of our manuscript and for highlighting the need to make the handling of the linearity constraint more explicit in the translation and its proof. We will revise the relevant sections to address this point directly.

read point-by-point responses

  1. Referee: [§4.1–4.3] §4.1–4.3 (the translation and its correctness proof): the argument that the mapping preserves satisfiability in both directions must explicitly address how the linearity constraint on plans is enforced inside S5 models; if S5 equivalence classes can encode branching or non-linear executions not permitted by the original semantics, then membership in NP via the S5 reduction or the hardness direction would fail to follow.

    Authors: We agree that the current write-up of the translation in §4.1–4.3 would benefit from an explicit discussion of how linearity is preserved. In the revised manuscript we will insert a short additional paragraph (and, if space permits, a supporting lemma) immediately after the definition of the translation. The added text will note that the S5 models arising from the reduction are constructed so that each equivalence class corresponds to a single linear sequence of worlds; the translation of the knowing-how operator uses a chain of distinct propositional atoms that mark successive steps along that sequence. Consequently, any satisfying assignment in the S5 model can be read off as a linear plan, and conversely any linear plan yields an S5 model whose equivalence class contains only the worlds reachable by that same linear execution. This construction rules out branching or non-linear paths inside the translated formulas, thereby preserving both directions of the satisfiability equivalence and the NP-completeness claim. revision: yes

Circularity Check

0 steps flagged

No significant circularity; reduction to independently known S5 result

full rationale

The paper derives NP-completeness of knowing-how satisfiability by exhibiting a translation into S5 modal logic whose satisfiability problem is already established in the literature as NP-complete. No step in the provided abstract or described proof chain reduces a prediction or central claim to a fitted parameter, self-defined quantity, or load-bearing self-citation whose justification loops back to the present paper. The translation is presented as an instrumental tool that preserves the linear-plan semantics, and the complexity bound is imported from external modal-logic results rather than being manufactured internally. This is the most common honest non-finding: the derivation remains self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The claim rests on the domain assumption of linear-plan semantics for knowing-how and on the correctness of the S5 translation; no free parameters or new entities are introduced.

axioms (1)
  • domain assumption Standard semantics for knowing-how assertions based on linear plans
    Invoked as the interpretation under which satisfiability is defined.

pith-pipeline@v0.9.0 · 5603 in / 1080 out tokens · 57610 ms · 2026-05-20T01:35:37.482406+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

118 extracted references · 118 canonical work pages

  1. [1]

    Gu and Y

    T. Gu and Y. Wang , title =. Advances in Modal Logic (. 2016 , publisher =

    work page 2016

  2. [2]

    Belardinelli, Francesco and Dima, Catalin and Murano, Aniello , booktitle =

    work page

  3. [3]

    Autonomous Agents and Multi-Agent Systems , volume =

    Andreas Herzig , title =. Autonomous Agents and Multi-Agent Systems , volume =

    work page

  4. [4]

    Epistemic Logic

    Paul Gochet and Pascal Gribomont. Epistemic Logic. Handbook of the History of Logic

    work page

  5. [5]

    Acta Philosophica Fennica , year =

    Wolfgang Lenzen , title =. Acta Philosophica Fennica , year =

    work page

  6. [6]

    and Mendelsohn, Richard L , title =

    Fitting, Melvin. and Mendelsohn, Richard L , title =. 1998 , series =

    work page 1998

  7. [7]

    Jaakko Hintikka , title =

    work page

  8. [8]

    D. E. Smith and D. S. Weld , title =. 15th National Conference on Artificial Intelligence and 10th Innovative Applications of Artificial Intelligence Conference (

    work page

  9. [9]

    Goranko and S

    V. Goranko and S. Passy , title =. Journal of Logic and Computation , volume =

    work page

  10. [10]

    Di Tillio and J

    A. Di Tillio and J. Y. Halpern and D. Samet , title =. Games and Economic Behavior , volume =

    work page

  11. [11]

    Proceedings of DEON 08 , pages =

    Jan Broersen , title =. Proceedings of DEON 08 , pages =

    work page

  12. [12]

    2014 , note =

    Shihao Xiong , title =. 2014 , note =

    work page 2014

  13. [13]

    Yifeng Ding , title =

    work page

  14. [14]

    and Lomuscio, A

    van der Hoek, W. and Lomuscio, A. , title =. 2nd International Conference on Autonomous Agents and MultiAgent Systems (. 2003 , pages =

    work page 2003

  15. [15]

    1966 , author=

    Contingency and non-contingency bases for normal modal logics , journal=. 1966 , author=

    work page 1966

  16. [16]

    Wang , title =

    Y. Wang , title =. Synthese , volume =

    work page

  17. [17]

    Wang , title =

    Y. Wang , title =. 5th International Workshop on Logic, Rationality, and Interaction (

    work page

  18. [18]

    van der Hoek and A

    W. van der Hoek and A. Lomuscio. A Logic For Ignorance. Electronic Notes in Theoretical Computer Science. 2004

    work page 2004

  19. [19]

    Handbook of Epistemic Logic , booktitle =

    work page

  20. [20]

    Y. Wang. Beyond knowing that: a new generation of epistemic logics. J. Hintikka on knowledge and game theoretical semantics. 2018

    work page 2018

  21. [21]

    Jamroga and W

    W. Jamroga and W. van der Hoek , title =. Fundamenta Informaticae , volume =

    work page

  22. [22]

    Naumov and J

    P. Naumov and J. Tao , title =. Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems,

    work page

  23. [23]

    Naumov and J

    P. Naumov and J. Tao , title =. 17th International Conference on Autonomous Agents and MultiAgent Systems (. 2018 , publisher =

    work page 2018

  24. [24]

    Action and Knowledge in Alternating-Time Temporal Logic , journal =

    Thomas. Action and Knowledge in Alternating-Time Temporal Logic , journal =. 2006 , url =. doi:10.1007/s11229-005-3875-8 , timestamp =

    work page doi:10.1007/s11229-005-3875-8 2006

  25. [25]

    Fantl , title =

    J. Fantl , title =. Philosophy Compass , volume =

    work page

  26. [26]

    Wang and J

    Y. Wang and J. Fan , title =. Proceedings of IJCAI 13 , year =

    work page

  27. [27]

    Wang and J

    Y. Wang and J. Fan , title =. Advances in Modal Logic Vol. 10 , pages =

    work page

  28. [28]

    and Wang, Y

    Fan, J. and Wang, Y. and van Ditmarsch, H. , title =. The Review of Symbolic Logic , volume =. 2015 , issn =

    work page 2015

  29. [29]

    Wang , title =

    Y. Wang , title =. Proceedings of ICLA 2015 , pages =

    work page 2015

  30. [30]

    The Review of Symbolic Logic , volume=

    The logic of justification , author=. The Review of Symbolic Logic , volume=. 2008 , doi =

    work page 2008

  31. [31]

    The Philosophical Forum , pages =

    Tszyuen Lau and Yanjing Wang , title =. The Philosophical Forum , pages =

    work page

  32. [32]

    15th Conference on Theoretical Aspects of Knowledge and Rationality (

    Quan Yu and Yanjun Li and Yanjing Wang , title =. 15th Conference on Theoretical Aspects of Knowledge and Rationality (. 2016 , pages =

    work page 2016

  33. [33]

    Advances in Modal Logic Vol.\ 9 , year =

    Yanjing Wang and Yanjun Li , title =. Advances in Modal Logic Vol.\ 9 , year =

    work page

  34. [34]

    Halpern and R

    J.Y. Halpern and R. Pucella , journal =. Dealing with logical omniscience: Expressiveness and pragmatics , year =

    work page

  35. [35]

    Wang , title =

    Y. Wang , title =. Proceedings Sixteenth Conference on Theoretical Aspects of Rationality and Knowledge,. 2017 , OPTcrossref =

    work page 2017

  36. [36]

    Li and Y

    Y. Li and Y. Wang , title =. 2017 , booktitle =

    work page 2017

  37. [37]

    Y. Li. Stopping Means Achieving: A Weaker Logic of Knowing How. Studies in Logic. 2017

    work page 2017

  38. [38]

    Hintikka

    J. Hintikka. The Semantics of Questions and the Questions of Semantics: Case Studies in the Interrelations of Logic, Semantics and Syntax

    work page

  39. [39]

    Von Wright, G. H. , citeulike-article-id =. An Essay in Modal Logic , year =

    work page

  40. [40]

    and Kozen, D

    Harel, D. and Kozen, D. and Tiuryn, J. , day =. Dynamic Logic , doi =

    work page

  41. [41]

    van Ditmarsch and W

    H. van Ditmarsch and W. van der Hoek and B. Kooi , isbn =. Dynamic Epistemic Logic , doi =

    work page

  42. [42]

    Herzig and E

    A. Herzig and E. Lorini and D. Walther , title =. Proceedings of LORI 2013 , pages =

    work page 2013

  43. [43]

    Using STIT Theory to Talk About Strategies

    Broersen, Jan and Herzig, Andreas. Using STIT Theory to Talk About Strategies. Models of Strategic Reasoning: Logics, Games, and Communities. 2015

    work page 2015

  44. [44]

    Harel , booktitle =

    D. Harel , booktitle =. Dynamic Logic , year =

    work page

  45. [45]

    Handbook of Modal Logic , volume =

    Blackburn, Patrick and van Benthem, Johan and Wolter, Frank , citeulike-article-id =. Handbook of Modal Logic , volume =

    work page

  46. [46]

    and Otto, M

    Goranko, V. and Otto, M. , booktitle =. Model Theory of Modal Logic , volume =

    work page

  47. [47]

    and de Rijke, M

    Blackburn, P. and de Rijke, M. and Venema, Y. , howpublished =. Modal Logic , OPTdoi =

    work page

  48. [48]

    Cooperation, Knowledge, and Time: Alternating-Time Temporal Epistemic Logic and Its Applications , year =

    Wiebe van der Hoek and Michael Wooldridge , journal =. Cooperation, Knowledge, and Time: Alternating-Time Temporal Epistemic Logic and Its Applications , year =

    work page

  49. [49]

    Blackburn and J

    P. Blackburn and J. van Benthem , title =. Handbook of Modal Logic , publisher =. 2006 , doi =

    work page 2006

  50. [50]

    Meyer and Wiebe van Der Hoek , title =

    John-Jules Ch. Meyer and Wiebe van Der Hoek , title =. 1995 , isbn =

    work page 1995

  51. [51]

    Alternating-time temporal logics with irrevocable strategies , booktitle =

    Thomas. Alternating-time temporal logics with irrevocable strategies , booktitle =. 2007 , OPTcrossref =

    work page 2007

  52. [52]

    Areces and R

    C. Areces and R. Fervari and A. R. Saravia and F. R. Vel. Uncertainty-Based Semantics for Multi-Agent Knowing How Logics , booktitle =

    work page

  53. [53]

    Journal of Applied Logic , volume =

    Jan Broersen , title =. Journal of Applied Logic , volume =. 2011 , url =. doi:10.1016/j.jal.2010.06.002 , timestamp =

    work page doi:10.1016/j.jal.2010.06.002 2011

  54. [54]

    Journal of Philosophical Logic , volume =

    Jan Broersen , title =. Journal of Philosophical Logic , volume =. 2011 , url =. doi:10.1007/s10992-011-9190-6 , timestamp =

    work page doi:10.1007/s10992-011-9190-6 2011

  55. [55]

    Stit, Iit, and Deontic logic for Action Types

    Bentzen, Martin Mose. Stit, Iit, and Deontic logic for Action Types. 2010

    work page 2010

  56. [56]

    , Date-Added =

    von Wright, G. , Date-Added =. Mind , Title =

    work page

  57. [57]

    Theorie Des Propositions Normatives , Volume =

    Kalinowski, Jerzy , Doi =. Theorie Des Propositions Normatives , Volume =. Studia Logica , Number =. 1953 , Bdsk-Url-1 =

    work page 1953

  58. [58]

    Uber den Modalkalk\

    Becker, Oskar , Publisher =. Untersuchungen \"Uber den Modalkalk\"ul , Year =

    work page

  59. [59]

    Handbook of Philosophical Logic: Volume 8 , Date-Added =

    Deontic Logic , Year =. Handbook of Philosophical Logic: Volume 8 , Date-Added =

    work page

  60. [60]

    Deontic Logic: A Personal View , Volume =

    von Wright, George , Journal =. Deontic Logic: A Personal View , Volume =

    work page

  61. [61]

    Agency and Deontic Logic , author =

    work page

  62. [62]

    Theoria , year=

    Seeing To it That: A Canonical Form for Agentives , author=. Theoria , year=

    work page

  63. [63]

    , citeulike-article-id =

    Hintikka, J. , citeulike-article-id =. Knowledge and Belief , year =

    work page

  64. [64]

    Halpern and Yoram Moses and Moshe Y

    Ronald Fagin and Joseph Y. Halpern and Yoram Moses and Moshe Y. Vardi , title =. 1995 , doi =

    work page 1995

  65. [65]

    Journal of Applied Non-Classical Logics , volume =

    Emiliano Lorini , title =. Journal of Applied Non-Classical Logics , volume =. 2013 , doi =

    work page 2013

  66. [66]

    Complexity Results of

    Fran. Complexity Results of. Studia Logica , volume =. 2012 , doi =

    work page 2012

  67. [67]

    Journal of Philosophical Logic , volume =

    Philippe Balbiani and Andreas Herzig and Nicolas Troquard , title =. Journal of Philosophical Logic , volume =. 2008 , doi =

    work page 2008

  68. [68]

    Properties of logics of individual and group agency , booktitle =

    Andreas Herzig and Fran. Properties of logics of individual and group agency , booktitle =. 2008 , url =

    work page 2008

  69. [69]

    2000 , isbn =

    Harel, David and Tiuryn, Jerzy and Kozen, Dexter , title =. 2000 , isbn =

    work page 2000

  70. [70]

    International Journal of Foundations of Computer Science , volume =

    Arne Meier and Michael Thomas and Heribert Vollmer and Martin Mundhenk , title =. International Journal of Foundations of Computer Science , volume =. 2009 , doi =

    work page 2009

  71. [71]

    2013 , volume =

    Handbook of Deontic Logic and Normative Systems , booktitle =. 2013 , volume =

    work page 2013

  72. [72]

    2021 , volume =

    Handbook of Deontic Logic and Normative Systems , booktitle =. 2021 , volume =

    work page 2021

  73. [73]

    Handbook of Normative Multiagent Systems , booktitle =

    work page

  74. [74]

    Journal of Economic Theory , volume =

    Knowing Whether, Knowing That, and The Cardinality of State Spaces , author=. Journal of Economic Theory , volume =. 1996 , doi=

    work page 1996

  75. [75]

    Synthese , volume =

    Chao Xu and Yanjing Wang and Thomas Studer , title =. Synthese , volume =

    work page

  76. [76]

    Advances in Modal Logic (

    Alexandru Baltag , title =. Advances in Modal Logic (. 2016 , publisher =

    work page 2016

  77. [77]

    Knowing Values and Public Inspection , booktitle =

    Jan van Eijck and Malvin Gattinger and Yanjing Wang , editor =. Knowing Values and Public Inspection , booktitle =. 2017 , url =. doi:10.1007/978-3-662-54069-5\_7 , timestamp =

    work page doi:10.1007/978-3-662-54069-5 2017

  78. [78]

    , title =

    Fantl, J. , title =. The Stanford Encyclopedia of Philosophy , howpublished =. 2021 , edition =

    work page 2021

  79. [79]

    Hayes , title =

    John McCarthy and Patrick J. Hayes , title =. Machine Intelligence , year =

    work page

  80. [80]

    A formal theory of knowledge and action , publisher =

    Moore, Robert , booktitle =. A formal theory of knowledge and action , publisher =

    work page

Showing first 80 references.