An implementation of hyper-resolution

DOI10.1016/0898-1221(75)90019-XzbMath0339.68060OpenAlexW2066125705MaRDI QIDQ1231393

Ross A. Overbeek

Publication date: 1975

Published in: Computers \& Mathematics with Applications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0898-1221(75)90019-x

Mathematics Subject Classification ID

Related Items (6)

The anatomy of vampire. Implementing bottom-up procedures with code trees ⋮ Complexity and related enhancements for automated theorem-proving programs ⋮ From LCF to Isabelle/HOL ⋮ Larry Wos: visions of automated reasoning ⋮ The problem of naming and function replacement ⋮ The problem of choosing the type of subsumption to use

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A New Class of Automated Theorem-Proving Algorithms
• A Machine-Oriented Logic Based on the Resolution Principle
• The Concept of Demodulation in Theorem Proving

This page was built for publication: An implementation of hyper-resolution