SOLAR: An automated deduction system for consequence finding

DOI10.3233/AIC-2010-0465zbMath1205.68362OpenAlexW1795691572MaRDI QIDQ3568229

Koji Iwanuma, Hidetomo Nabeshima, Katsumi Inoue, Oliver Ray

Publication date: 17 June 2010

Published in: AI Communications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.3233/aic-2010-0465

zbMATH Keywords

theorem provingfirst-order logicSOL calculusconsequence findingconnection tableaux

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27)

Related Items

Translation of first order formulas into ground formulas via a completion theory ⋮ Quantifier-Free Equational Logic and Prime Implicate Generation ⋮ Completing causal networks by meta-level abduction ⋮ Meta-interpretive learning: application to grammatical inference ⋮ Abductive Reasoning on Molecular Interaction Maps ⋮ SOLAR ⋮ Connection-minimal abduction in \(\mathcal{EL}\) via translation to FOL

Uses Software

• TPTP
• E Theorem Prover