An implementation of hyper-resolution

DOI10.1016/0898-1221(75)90019-XMaRDI QIDQ1231393zbMATH OpenOpenAlexFDO

Authors 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

General topics in the theory of software (68N01)

Cites work

• scientific article; zbMATH DE number 3473265 (Why is no real title available?)
• scientific article; zbMATH DE number 3254919 (Why is no real title available?)
• scientific article; zbMATH DE number 3278281 (Why is no real title available?)
• scientific article; zbMATH DE number 3303654 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• A Machine-Oriented Logic Based on the Resolution Principle
• A New Class of Automated Theorem-Proving Algorithms
• The Concept of Demodulation in Theorem Proving

Cited in

(6)

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1231393)