scientific article; zbMATH DE number 1303349

zbMath0926.03008MaRDI QIDQ4249902

Yoshihiko Ohta, Katsumi Inoue, Ryuzo Hasegawa

Publication date: 15 September 1999

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

automated theorem provingmodel generationnon-Horn magic setspruning redundant branches of a proof treeweak relevancy testing

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy, 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, A relevance restriction strategy for automated deduction