Mechanical Theorem-Proving by Model Elimination

DOI10.1145/321450.321456zbMATH Open0162.02804DBLPjournals/jacm/Loveland68OpenAlexW2005090804WikidataQ56814468 ScholiaQ56814468MaRDI QIDQ5544307FDOQ5544307

Authors: Donald W. Loveland 

Publication date: 1968

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/321450.321456

zbMATH Keywords

languages, automata, networks

Cited In (38)

• Simultaneous rigid E-unification is undecidable
• A typed resolution principle for deduction with conditional typing theory
• Model elimination without contrapositives
• Case-free programs: An abstraction of definite horn programs
• Decidability and complexity of simultaneous rigid E-unification with one variable and related results
• An annotated logic theorem prover for an extended possibilistic logic
• From Schütte’s Formal Systems to Modern Automated Deduction
• Local simplification
• Clause trees: A tool for understanding and implementing resolution in automated reasoning
• Near-Horn Prolog and the ancestry family of procedures
• Filter-based resolution principle for lattice-valued propositional logic LP\((X)\)
• The proof complexity of analytic and clausal tableaux
• Ordered tableaux: extensions and applications
• leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
• What you always wanted to know about rigid \(E\)-unification
• Detecting non-provable goals
• Machine learning guidance for connection tableaux
• Hierarchical deduction
• Computing answers with model elimination
• Automatic acquisition of search guiding heuristics
• Optimizing proof search in model elimination
• An extension to linear resolution with selection function
• Refutation graphs
• Controlled integration of the cut rule into connection tableau calculi
• IeanCOP: lean connection-based theorem proving
• Subsumption-linear Q-resolution for QBF theorem proving
• Prolog technology for default reasoning: proof theory and compilation techniques
• Theorem proving with variable-constrained resolution
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Completeness results for inequality provers
• A Non-clausal Connection Calculus
• Controlled use of clausal lemmas in connection tableau calculi
• HOL Light: An Overview
• Automated inferencing
• The linked conjunct method for automatic deduction and related search techniques
• The undecidability of simultaneous rigid E-unification
• A relevance restriction strategy for automated deduction
• Linear and unit-resulting refutations for Horn theories

This page was built for publication: Mechanical Theorem-Proving by Model Elimination

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