The linked conjunct method for automatic deduction and related search techniques
From MaRDI portal
Publication:1836998
DOI10.1016/0898-1221(82)90042-6zbMath0506.68075OpenAlexW2050203572MaRDI QIDQ1836998
Publication date: 1982
Published in: Computers \& Mathematics with Applications (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0898-1221(82)90042-6
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (1)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Tautology testing with a generalized matrix reduction method
- Refutation graphs
- A unification algorithm for typed \(\overline\lambda\)-calculus
- Mechanizing \(\omega\)-order type theory through unification
- Theorem-Proving on the Computer
- Refutations by Matings
- A Search Technique for Clause Interconnectivity Graphs
- Towards feasible solutions of the tautology problem
- A Proof Procedure Using Connection Graphs
- A Machine-Oriented Logic Based on the Resolution Principle
- Mechanical Theorem-Proving by Model Elimination
- Resolution With Merging
- A Simplified Format for the Model Elimination Theorem-Proving Procedure
- A Computing Procedure for Quantification Theory
- Resolution in type theory
This page was built for publication: The linked conjunct method for automatic deduction and related search techniques
