Complete problems in the first-order predicate calculus

DOI10.1016/0022-0000(84)90010-2zbMath0592.03026OpenAlexW2066989651MaRDI QIDQ1075318

David Alan 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 computation (including implicit computational complexity) (03D15) Complexity of proofs (03F20)

Related Items

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Complexity results for classes of quantificational formulas
• Complete problems for deterministic polynomial time
• The complexity of propositional linear temporal logics
• Alternation
• Complexity classes and theories of finite models
• New problems complete for nondeterministic log space
• Turing machines and the spectra of first-order formulas
• A Machine-Oriented Logic Based on the Resolution Principle
• The complexity of theorem-proving procedures