scientific article; zbMATH DE number 1140676

zbMATH Open0895.03004MaRDI QIDQ4385441FDOQ4385441

Authors: Timothy J. Surendonk, John K. Slaney 

Publication date: 2 September 1998

Title of this publication is not available (Why is that?)

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

zbMATH Keywords

interpretationmodel generationcondensed detachmentautomatic theorem proverautomatic searching for proofSemantically Constrained Otter

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cited In (5)

• SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment
• Title not available (Why is that?)
• Title not available (Why is that?)
• Partition-based logical reasoning for first-order and propositional theories
• Title not available (Why is that?)

Uses Software

• OTTER
• FINDER
• SCOTT

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)