scientific article; zbMATH DE number 1303349

zbMATH Open0926.03008MaRDI QIDQ4249902FDOQ4249902

Yoshihiko Ohta, Katsumi Inoue, Ryuzo Hasegawa

Publication date: 15 September 1999

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

Recommendations

• Non-Horn magic sets to incorporate top-down inference into bottom-up theorem proving
• scientific article; zbMATH DE number 1341620
• MGTP: a model generation theorem prover. Its advanced features and applications
• A relevance restriction strategy for automated deduction
• SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy

zbMATH Keywords

model generationautomated theorem provingnon-Horn magic setspruning redundant branches of a proof treeweak relevancy testing

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cited In (6)

• MGTP: A model generation theorem prover — Its advanced features and applications —
• \(\mathcal I\)-SATCHMORE: An improvement of \(\mathcal A\)-SATCHMORE
• SATCHMORE: SATCHMO with RElevancy
• Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving
• SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy
• A relevance restriction strategy for automated deduction

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 Q4249902)