Geometric Resolution: A Proof Procedure Based on Finite Model Search
From MaRDI portal
Recommendations
Cited in
(20)- Invited Talk: Coherentisation of First-Order Logic
- Classical logic with partial functions
- Superposition for bounded domains
- Exploring theories with a model-finding assistant
- Classical logic with partial functions
- Deciding effectively propositional logic using DPLL and substitution sets
- Finding shortest proofs: An application of linked inference rules
- Computing finite models by reduction to function-free clause logic
- Efficiently checking propositional refutations in HOL theorem provers
- Automated generation of illustrated proofs in geometry and beyond
- Automated verification of refinement laws
- Bounded Relational Analysis of Free Data Types
- Model evolution with equality -- revised and implemented
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
- A multi-clause dynamic deduction algorithm based on standard contradiction separation rule
- Turning decision procedures into disprovers
- Automated generation of illustrations for synthetic geometry proofs
- Theorem proving as constraint solving with coherent logic
- On the mechanization of the proof of Hessenberg's theorem in coherent logic
- Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
This page was built for publication: Geometric Resolution: A Proof Procedure Based on Finite Model Search
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3613415)
