Using sophisticated models in resolution theorem proving

zbMATH Open0453.03014MaRDI QIDQ1148892FDOQ1148892

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 complete semantic back chaining proof system
• A semantic backward 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)