scientific article; zbMATH DE number 1140676

MaRDI QIDQ4385441zbMATH OpenFDO

Authors Timothy J. Surendonk, John K. Slaney

Publication date 2 September 1998

zbMATH Keywords

interpretationmodel generationcondensed detachmentautomatic theorem proverautomatic searching for proofSemantically Constrained Otter

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 1765689
• scientific article; zbMATH DE number 1809864
• Automatic theorem proving and OTTER
• Generating relevant models
• Efficient model generation through compilation

Cited in

(5)

• SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment
• scientific article; zbMATH DE number 1696802 (Why is no real title available?)
• scientific article; zbMATH DE number 1389646 (Why is no real title available?)
• Partition-based logical reasoning for first-order and propositional theories
• scientific article; zbMATH DE number 1765689 (Why is no real title available?)

Describes a project that uses

Uses Software

• SCOTT
• FINDER
• OTTER

This page was built for publication:

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