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