Mechanical Theorem-Proving by Model Elimination
From MaRDI portal
Publication:5544307
DOI10.1145/321450.321456zbMath0162.02804OpenAlexW2005090804WikidataQ56814468 ScholiaQ56814468MaRDI QIDQ5544307
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
Related Items
Completeness results for inequality provers, Controlled integration of the cut rule into connection tableau calculi, Hierarchical deduction, HOL Light: An Overview, Filter-based resolution principle for lattice-valued propositional logic LP\((X)\), An annotated logic theorem prover for an extended possibilistic logic, Linear and unit-resulting refutations for Horn theories, Near-Horn Prolog and the ancestry family of procedures, Clause trees: A tool for understanding and implementing resolution in automated reasoning, Computing answers with model elimination, IeanCOP: lean connection-based theorem proving, Subsumption-linear Q-resolution for QBF theorem proving, Ordered tableaux: Extensions and applications, An extension to linear resolution with selection function, leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions), The undecidability of simultaneous rigid E-unification, A Non-clausal Connection Calculus, Optimizing proof search in model elimination, Controlled use of clausal lemmas in connection tableau calculi, Refutation graphs, Machine learning guidance for connection tableaux, Model elimination without contrapositives, Detecting non-provable goals, Local simplification, Prolog technology for default reasoning: proof theory and compilation techniques, What you always wanted to know about rigid E-unification, Theorem proving with variable-constrained resolution, Decidability and complexity of simultaneous rigid E-unification with one variable and related results, The proof complexity of analytic and clausal tableaux, The linked conjunct method for automatic deduction and related search techniques, From Schütte’s Formal Systems to Modern Automated Deduction, A typed resolution principle for deduction with conditional typing theory, Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\), Automated inferencing, A relevance restriction strategy for automated deduction
