Reduction rules for resolution-based systems
- 31 July 1991
- journal article
- Published by Elsevier in Artificial Intelligence
- Vol. 50 (2) , 141-181
- https://doi.org/10.1016/0004-3702(91)90098-5
Abstract
No abstract availableKeywords
This publication has 15 references indexed in Scilit:
- A new reduction rule for the connection graph proof procedureJournal of Automated Reasoning, 1988
- On the efficiency of subsumption algorithmsJournal of the ACM, 1985
- Properties of substitutions and unificationsJournal of Symbolic Computation, 1985
- On Matrices with ConnectionsJournal of the ACM, 1981
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting SystemsJournal of the ACM, 1980
- Using rewriting rules for connection graphs to prove theoremsArtificial Intelligence, 1979
- A Proof Procedure Using Connection GraphsJournal of the ACM, 1975
- Automatic theorem-proving and the decision problemPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1973
- Z-Resolution: Theorem-Proving with Compiled AxiomsJournal of the ACM, 1973
- Linear resolution with selection functionArtificial Intelligence, 1972