2026-09-15T15:40:15Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:25430 2026-09-05T19:16:22Z ddc:004 open_access

Hereditary First-Order Logic: the Tractable Quantifier Prefix Classes Bodirsky, Manuel Guzmán-Pro, Santiago Quantifier prefix first-order Logic Computational Complexity Polynomial-time algorithm coNP-completeness 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). Schloss Dagstuhl – Leibniz-Zentrum für Informatik Manuel Bodirsky and Santiago Guzmán-Pro 2026 Is Part Of LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2026.6 urn:nbn:de:0030-drops-254308 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.6 eng https://creativecommons.org/licenses/by/4.0/legalcode