A Semantically Guided Deductive System for Automatic Theorem Proving

DOI10.1109/TC.1976.1674613zbMath0324.68052OpenAlexW2010917637MaRDI QIDQ4088303

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)

Related Items

A review and prospect of readable machine proofs for geometry theorems, 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