Complete problems in the first-order predicate calculus

DOI10.1016/0022-0000(84)90010-2MaRDI QIDQ1075318zbMATH OpenOpenAlexFDO

Authors David A. Plaisted

Publication date 1984

Published in Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/2027/uiuo.ark:/13960/t4qj90q4p

zbMATH Keywords

complete for various complexity classesfirst-order predicate calculus formulae that areresolution theorem provingsystemsTuring machines

Mathematics Subject Classification ID

Classical first-order logic (03B10) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Complexity of computation (including implicit computational complexity) (03D15) Complexity of proofs (03F20) Analysis of algorithms and problem complexity (68Q25)

Review text

Neben den klassischen Komplexitätsklassen P und NP wird seit längerem eine Reihe weiterer solcher Klassen untersucht. Der Autor stellt einen Zusammenhang zwischen einigen Formeln der Prädikatenlogik 1. Stufe und Turingmaschinen her. Diese zunächst sehr abstrakte Aussage wird dazu benutzt, eine natürliche Hierarchie vollständiger Probleme für die Klassen P, NP, PSPACE, deterministische und nichtdeterministische exponentielle Zeit, deterministische und nichtdeterministische doppelt exponentielle Zeit, DLOGSPACE und NLOGSPACE zu entwickeln. Eine ähnliche Hierarchie ergibt sich, wenn nach der Existenz von Beweisen einer vorgegebenen maximalen Tiefe für die oben genannten Formeln gefragt wird. Spezielle Resultate betreffen u.a. ein erstes Beispiel eines vollständigen Problems für EXPSPACE. Eine mögliche Anwendung dieser Ergebnisse liegt in der Beschleunigung von Beweisführungsprogrammen.

Recommendations

• Logics for complexity classes
• scientific article; zbMATH DE number 3885864
• scientific article; zbMATH DE number 3952713
• scientific article; zbMATH DE number 3898847
• Satisfiability of formulae with one \(\forall\) is decidable in exponential time

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• Alternation
• Complete problems for deterministic polynomial time
• Complexity classes and theories of finite models
• Complexity results for classes of quantificational formulas
• scientific article; zbMATH DE number 3664335 (Why is no real title available?)
• scientific article; zbMATH DE number 3731310 (Why is no real title available?)
• scientific article; zbMATH DE number 3474957 (Why is no real title available?)
• scientific article; zbMATH DE number 3550181 (Why is no real title available?)
• scientific article; zbMATH DE number 3569825 (Why is no real title available?)
• scientific article; zbMATH DE number 3639144 (Why is no real title available?)
• scientific article; zbMATH DE number 3254919 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• New problems complete for nondeterministic log space
• The complexity of propositional linear temporal logics
• The complexity of theorem-proving procedures
• Turing machines and the spectra of first-order formulas

Cited in

(10)

• Equational methods in first order predicate calculus
• Isomorphisms and 1-L reductions
• Complexity results for classes of quantificational formulas
• Inference flexibility in Horn clause knowledge bases and the simplex method
• Problem solving by searching for models with a theorem prover
• SCL clause learning from simple models
• Sufficient-completeness, ground-reducibility and their complexity
• Meeting of the Association for Symbolic Logic, Stanford, California, 1985
• Classifying the computational complexity of problems
• A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic

This page was built for publication: Complete problems in the first-order predicate calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1075318)