Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving

DOI10.1007/3-540-63104-6_18zbMath1430.68410OpenAlexW2098536959MaRDI QIDQ5234700

Yoshihiko Ohta, Katsumi Inoue, Miyuki Koshimura, Ryuzo Hasegawa

Publication date: 1 October 2019

Published in: Automated Deduction—CADE-14 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-63104-6_18

zbMATH Keywords

deductive databaseproof treeHorn clausemodel candidaterelevancy testing

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

Blocking and other enhancements for bottom-up model generation methods

Uses Software

• TPTP
• SATCHMO
• MGTP

Cites Work

• Unnamed Item
• Unnamed Item
• An efficient strategy for non-Horn deductive databases
• The TPTP problem library. CNF release v1. 2. 1
• Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction
• The Alexander Method - a technique for the processing of recursive axioms in deductive databases
• SATCHMORE: SATCHMO with RElevancy
• On the power of magic
• Minimal model generation with positive unit hyper-resolution tableaux

This page was built for publication: Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving