New methods for computing inferences in first order logic

DOI10.1007/BF02027814MaRDI QIDQ1309900zbMATH OpenFDO

Authors John N. Hooker

Publication date 20 December 1993

Published in Annals of Operations Research (Search for Journal in Brave)

zbMATH Keywords

satisfiability algorithmsdecidable fragment of first order logicpartial instantiation

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Partial instantiation methods for inference in first-order logic
• Algorithms for testing satisfiability formulas
• Computing definite logic programs by partial instantiation
• Combining instance generation and resolution
• A Computational Study of Satisfiability Algorithms for Propositional Logic

Cites work

• scientific article; zbMATH DE number 4053069 (Why is no real title available?)
• scientific article; zbMATH DE number 1324220 (Why is no real title available?)
• A linear programming approach to reasoning about probabilities
• A note on the Entscheidungsproblem
• Algorithms for testing the satisfiability of propositional formulae
• Boole's logic and probability. A critical exposition from the standpoint of contemporary algebra, logic and probability theory
• Branch-and-cut solution of inference problems in propositional logic
• Computational experience with an interior point algorithm on the satisfiability problem
• Extended Horn sets in propositional logic
• Input Proofs and Rank One Cutting Planes
• Probabilistic logic
• Probabilistic satisfiability
• Resolution vs. cutting plane solution of inference problems: Some computational experience
• Solving propositional satisfiability problems
• Solving the incremental satisfiability problem
• Some results and experiments in programming techniques for propositional logic

Cited in

(9)

• Many-valued logic and mixed integer programming
• Computer Science Logic
• Partition-based logical reasoning for first-order and propositional theories
• Partial instantiation methods for inference in first-order logic
• Combining instance generation and resolution
• Computing definite logic programs by partial instantiation
• Non-cyclic sorts for first-order satisfiability
• An approximative inference method for solving \(\exists \forall \)SO satisfiability problems
• Literal Projection for First-Order Logic

This page was built for publication: New methods for computing inferences in first order logic

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