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

systemsTuring machinesresolution theorem provingcomplete for various complexity classesfirst-order predicate calculus formulae that are

Mathematics Subject Classification ID

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

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

• 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?)
• 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
• 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)

• A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
• SCL clause learning from simple models
• Meeting of the Association for Symbolic Logic, Stanford, California, 1985
• 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
• Sufficient-completeness, ground-reducibility and their complexity
• Classifying the computational complexity of problems
• Equational methods in first order predicate calculus
• Isomorphisms and 1-L reductions

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)