An Evaluation of an Implementation of Qualified Hyperresolution
- 1 August 1976
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Computers
- Vol. C-25 (8) , 835-843
- https://doi.org/10.1109/TC.1976.1674702
Abstract
A new inference rule for resolution based theorem proving, termed qualified hyperresolution, is presented from a practical point of view. The method of qualification is intended to deal with clause sets involving not-everywhere-defined functions. Two examples illustrating the effects of the method are discussed in detail. The potential practical value of the method is indicated by substantial improvements over the performance of ordinary hyperresolution obtained in five test problems.Keywords
This publication has 5 references indexed in Scilit:
- Problems and Experiments for and with Automated Theorem-Proving ProgramsIEEE Transactions on Computers, 1976
- An implementation of hyper-resolutionComputers & Mathematics with Applications, 1975
- Splitting and reduction heuristics in automatic theorem provingArtificial Intelligence, 1971
- The Concept of Demodulation in Theorem ProvingJournal of the ACM, 1967
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965