A Semantically Guided Deductive System for Automatic Theorem Proving

DOI10.1109/TC.1976.1674613MaRDI QIDQ4088303zbMATH OpenOpenAlexFDO

Authors Raymond Reiter

Publication date 1976

Published in IEEE Transactions on Computers (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1109/tc.1976.1674613

Mathematics Subject Classification ID

Proof theory and constructive mathematics (03F99)

Cited in

(7)

• A simplified problem reduction format
• A semantic backward chaining proof system
• A theory of abstraction
• Non-resolution theorem proving
• The Q^* algorithm - a search strategy for a deductive question-answering system
• A review and prospect of readable machine proofs for geometry theorems
• A complete semantic back chaining proof system

This page was built for publication: A Semantically Guided Deductive System for Automatic Theorem Proving

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