Geometric Resolution: A Proof Procedure Based on Finite Model Search
From MaRDI portal
Publication:3613415
DOI10.1007/11814771_28zbMath1222.68378OpenAlexW1495157771MaRDI QIDQ3613415
Publication date: 12 March 2009
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/11814771_28
Related Items
Exploring Theories with a Model-Finding Assistant, Invited Talk: Coherentisation of First-Order Logic, A multi-clause dynamic deduction algorithm based on standard contradiction separation rule, Automated generation of illustrated proofs in geometry and beyond, Model evolution with equality -- revised and implemented, Classical logic with partial functions, Deciding Effectively Propositional Logic Using DPLL and Substitution Sets, On the mechanization of the proof of Hessenberg's theorem in coherent logic, Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning, Superposition for Bounded Domains, Deciding effectively propositional logic using DPLL and substitution sets, Classical Logic with Partial Functions, Bounded Relational Analysis of Free Data Types, Efficiently checking propositional refutations in HOL theorem provers, Computing finite models by reduction to function-free clause logic, Subsumption Algorithms for Three-Valued Geometric Resolution, Automated verification of refinement laws, Theorem proving as constraint solving with coherent logic
Uses Software
