Document Open Access Logo

Hereditary First-Order Logic: the Tractable Quantifier Prefix Classes

Authors Manuel Bodirsky , Santiago Guzmán-Pro

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.6.pdf
  • Filesize: 0.9 MB
  • 20 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Complexity theory and logic
Keywords
  • Quantifier prefix
  • first-order Logic
  • Computational Complexity
  • Polynomial-time algorithm
  • coNP-completeness

Metrics

Abstract

Many computational problems can be modelled as the class of all finite structures A that satisfy a fixed first-order sentence ϕ hereditarily, i.e., we require that every (induced) substructure of A satisfies ϕ. We call the corresponding computational problem the hereditary model checking problem for ϕ, and denote it by Her(ϕ).
We present a complete description of the quantifier prefixes for ϕ such that Her(ϕ) is in P; we show that for every other quantifier prefix there exists a formula ϕ with this prefix such that Her(ϕ) is coNP-complete. Specifically, we show that if Q is of the form ∀*∃∀* or of the form ∀*∃*, then Her(ϕ) can be solved in polynomial time whenever the quantifier prefix of ϕ is Q. Otherwise, Q contains ∃∃∀ or ∃∀∃ as a subword, and in this case, there is a first-order formula ϕ whose quantifier prefix is Q and Her(ϕ) is coNP-complete. Moreover, we show that there is no algorithm that decides for a given first-order formula ϕ whether Her(ϕ) is in P (unless P=NP).

Cite As Get BibTex

Manuel Bodirsky and Santiago Guzmán-Pro. Hereditary First-Order Logic: the Tractable Quantifier Prefix Classes. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 6:1-6:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.6

Author Details

Manuel Bodirsky
  • Institut für Algebra, TU Dresden, Germany
Santiago Guzmán-Pro
  • Institut für Algebra, TU Dresden, Germany

Funding

Both authors have been funded by the European Research Council (Project POCOCOP, ERC Synergy Grant 101071674). Views and opinions expressed are however those of the authors only and do not necessarily reflect those of the European Union or the European Research Council Executive Agency. Neither the European Union nor the granting authority can be held responsible for them.

Acknowledgements

This is a low-co2 research paper: https://tcs4f.org/low-co2-v1. This research was developed, written, submitted and presented without the use of air travel.

References

  1. Max Bannach, Florian Chudigiewitsch, and Till Tantau. On the descriptive complexity of vertex deletion problems. In Rastislav Královic and Antonín Kucera, editors, 49th International Symposium on Mathematical Foundations of Computer Science, MFCS 2024, August 26-30, 2024, Bratislava, Slovakia, volume 306 of LIPIcs, pages 17:1-17:14, Dagstuhl, Germany, 2024. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.MFCS.2024.17.
  2. Manuel Bodirsky. Complexity of Infinite-Domain Constraint Satisfaction. Lecture Notes in Logic (52). Cambridge University Press, Cambridge, United Kingdom; New York, NY, 2021. URL: https://doi.org/10.1017/9781107337534.
  3. Manuel Bodirsky and Santiago Guzmán-Pro. Hereditary First-Order Logic: the tractable quantifier prefix classes. Preprint arXiv:2411.10860, 2024. URL: https://doi.org/10.48550/arXiv.2411.10860.
  4. Manuel Bodirsky and Jan Kára. A fast algorithm and datalog inexpressibility for temporal reasoning. ACM Trans. Comput. Log., 11(3):15:1-15:21, 2010. URL: https://doi.org/10.1145/1740582.1740583.
  5. Manuel Bodirsky, Simon Knäuer, and Sebastian Rudolph. Datalog-expressibility for monadic and guarded second-order logic. In Nikhil Bansal, Emanuela Merelli, and James Worrell, editors, 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference), volume 198 of LIPIcs, pages 120:1-120:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. Preprint available at https://arxiv.org/abs/2010.05677. URL: https://doi.org/10.4230/LIPIcs.ICALP.2021.120.
  6. J. Adrian Bondy and Uppaluri S. R. Murty. Graph Theory. Graduate Texts in Mathematics. Springer, Berlin, 2008. URL: https://doi.org/10.1007/978-1-84628-970-5.
  7. Egon Börger, Erich Grädel, and Yuri Gurevich. The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, 1997. Google Scholar
  8. Heinz-Dieter Ebbinghaus and Jörg Flum. Finite model theory. Perspectives in Mathematical Logic. Springer, Berlin, Heidelberg, New York, 1995. Second edition. Google Scholar
  9. Thomas Eiter, Georg Gottlob, and Thomas Schwentick. The model checking problem for prefix classes of second-order logic: A survey. In Andreas Blass, Nachum Dershowitz, and Wolfgang Reisig, editors, Fields of Logic and Computation, Essays Dedicated to Yuri Gurevich on the Occasion of His 70th Birthday, volume 6300 of Lecture Notes in Computer Science, pages 227-250, Berlin, Heidelberg, 2010. Springer. URL: https://doi.org/10.1007/978-3-642-15025-8_13.
  10. Tomás Feder and Moshe Y. Vardi. The computational structure of monotone monadic SNP and constraint satisfaction: A study through datalog and group theory. SIAM J. Comput., 28(1):57-104, 1998. URL: https://doi.org/10.1137/S0097539794266766.
  11. Tomás Feder and Moshe Y. Vardi. Homomorphism closed vs. existential positive. In 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22-25 June 2003, Ottawa, Canada, Proceedings, pages 311-320. IEEE Computer Society, 2003. URL: https://doi.org/10.1109/LICS.2003.1210071.
  12. Fedor V. Fomin, Petr A. Golovach, and Dimitrios M. Thilikos. On the parameterized complexity of graph modification to first-order logic properties. Theory Comput. Syst., 64(2):251-271, 2020. URL: https://doi.org/10.1007/s00224-019-09938-8.
  13. Toshihiro Fujito. A unified approximation algorithm for node-deletion problems. Discret. Appl. Math., 86(2-3):213-231, 1998. URL: https://doi.org/10.1016/S0166-218X(98)00035-3.
  14. Georg Gottlob, Phokion G. Kolaitis, and Thomas Schwentick. Existential second-order logic over graphs: Charting the tractability frontier. J. ACM, 51(2):312-362, 2004. URL: https://doi.org/10.1145/972639.972646.
  15. Wilfrid Hodges. Model theory, volume 42 of Encyclopedia of mathematics and its applications. Cambridge University Press, Cambridge, 1993. Google Scholar
  16. Wilfrid Hodges. A shorter model theory. Cambridge University Press, Cambridge, 1997. Google Scholar
  17. Mukkai S. Krishnamoorthy and Narsingh Deo. Node-deletion np-complete problems. SIAM J. Comput., 8(4):619-625, 1979. URL: https://doi.org/10.1137/0208049.
  18. John M. Lewis and Mihalis Yannakakis. The node-deletion problem for hereditary properties is np-complete. J. Comput. Syst. Sci., 20(2):219-230, 1980. URL: https://doi.org/10.1016/0022-0000(80)90060-4.
  19. Christos H. Papadimitriou and Mihalis Yannakakis. Optimization, approximation, and complexity classes. J. Comput. Syst. Sci., 43(3):425-440, 1991. URL: https://doi.org/10.1016/0022-0000(91)90023-X.
  20. Venkatesh Raman, Saket Saurabh, and C. R. Subramanian. Faster fixed parameter tractable algorithms for finding feedback vertex sets. ACM Trans. Algorithms, 2(3):403-415, July 2006. URL: https://doi.org/10.1145/1159892.1159898.
  21. Bruce A. Reed, Kaleigh Smith, and Adrian Vetta. Finding odd cycle transversals. Oper. Res. Lett., 32(4):299-301, 2004. URL: https://doi.org/10.1016/j.orl.2003.10.009.
  22. Donald J. Rose. A note on consistent ordering and zero circulation. J. ACM, 18(4):573-575, 1971. URL: https://doi.org/10.1145/321662.321671.
  23. Donald J. Rose, Robert Endre Tarjan, and George S. Lueker. Algorithmic aspects of vertex elimination on graphs. SIAM J. Comput., 5(2):266-283, 1976. URL: https://doi.org/10.1137/0205021.
  24. Boris A. Trakhtenbrot. Understanding basic automata theory in the continuous time setting. Fundam. Informaticae, 62(1):69-121, 2004. (in Russian). URL: http://content.iospress.com/articles/fundamenta-informaticae/fi62-1-04.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact