scientific article; zbMATH DE number 1303349

MaRDI QIDQ4249902zbMATH OpenFDO

Authors Yoshihiko Ohta, Katsumi Inoue, Ryuzo Hasegawa

Publication date 15 September 1999

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)

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

Cited in

(6)

• \(\mathcal I\)-SATCHMORE: An improvement of \(\mathcal A\)-SATCHMORE
• SATCHMORE: SATCHMO with RElevancy
• MGTP: a model generation theorem prover. Its advanced features and applications
• 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)