Mechanical Theorem-Proving by Model Elimination
From MaRDI portal
Publication:5544307
Cited in
(38)- A typed resolution principle for deduction with conditional typing theory
- Simultaneous rigid E-unification is undecidable
- Decidability and complexity of simultaneous rigid E-unification with one variable and related results
- Model elimination without contrapositives
- Case-free programs: An abstraction of definite horn programs
- An annotated logic theorem prover for an extended possibilistic logic
- Local simplification
- Clause trees: A tool for understanding and implementing resolution in automated reasoning
- From Schütte’s Formal Systems to Modern Automated Deduction
- Filter-based resolution principle for lattice-valued propositional logic LP(X)
- Near-Horn Prolog and the ancestry family of procedures
- 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
- An extension to linear resolution with selection function
- Refutation graphs
- Automatic acquisition of search guiding heuristics
- Optimizing proof search in model elimination
- 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
- Automated inferencing
- The undecidability of simultaneous rigid E-unification
- HOL Light: An Overview
- The linked conjunct method for automatic deduction and related search techniques
- 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)
