The complexity of resource-bounded first-order classical logic

DOI10.1007/3-540-57785-8_131MaRDI QIDQ4942635zbMATH OpenFDO

Authors Jean Goubault-Larrecq

Publication date 16 March 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-57785-8_131

Mathematics Subject Classification ID

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)

Recommendations

• scientific article; zbMATH DE number 1037485
• Automated theorem proving by resolution in non-classical logics
• scientific article; zbMATH DE number 4155933
• scientific article; zbMATH DE number 1113998
• Automated complexity analysis based on ordered resolution

Cited in

(9)

• On the modelling of search in theorem proving -- towards a theory of strategy analysis
• A modal view on resource-bounded propositional logics
• Encoding first order proofs in SMT
• The limits of decidability for first order logic on CPDA graphs
• Protocol Verification Via Rigid/Flexible Resolution
• An \({\mathcal O}((n\log n)^3)\)-time transformation from Grz into decidable fragments of classical first-order logic
• The Exact Complexity of the First-Order Logic Definability Problem
• Proving with BDDs and control of information
• Finding connections via satisfiability solving

Describes a project that uses

Uses Software

• Ltur

This page was built for publication: The complexity of resource-bounded first-order classical logic

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