Using sophisticated models in resolution theorem proving

MaRDI QIDQ1148892zbMATH OpenFDO

Authors David M. Sandford

Publication date 1980

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

zbMATH Keywords

modelsresolution theorem provingsemantic functions

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to computer science (68-02) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Mechanization of proofs and logical operations (03B35)

Cited in

(4)

• A typed resolution principle for deduction with conditional typing theory
• A method for simultaneous search for refutations and models by equational constraint solving
• A semantic backward chaining proof system
• A complete semantic back chaining proof system

This page was built for publication: Using sophisticated models in resolution theorem proving

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