SOLAR (SOL for Advanced Reasoning) is a first-order clausal consequence finding system based on the SOL (Skip Ordered Linear) tableau calculus. The ability to find non-trivial consequences of an axiom set is useful in many applications of Artificial Intelligence such as theorem proving, query answering and nonmonotonic reasoning. SOL is a connection tableau calculus which is complete for finding the non-subsumed consequences of a clausal theory. SOLAR is an efficient implementation of SOL that employs several methods to prune away redundant branches of the search space. This paper introduces some of the key pruning and control strategies implemented in SOLAR and demonstrates their effectiveness on a collection of benchmark problems.

This software is also peer reviewed by journal TOMS.

References in zbMATH (referenced in 16 articles , 1 standard article )

Showing results 1 to 16 of 16.
Sorted by year (citations)

  1. Demolombe, Robert; Fariñas del Cerro, Luis; Obeid, Naji: Translation of first order formulas into ground formulas via a completion theory (2016)
  2. Echenim, Mnacho; Peltier, Nicolas; Tourret, Sophie: Quantifier-free equational logic and prime implicate generation (2015)
  3. Muggleton, Stephen H.; Lin, Dianhuan; Pahlavi, Niels; Tamaddoni-Nezhad, Alireza: Meta-interpretive learning: application to grammatical inference (2014)
  4. Inoue, Katsumi; Doncescu, Andrei; Nabeshima, Hidetomo: Completing causal networks by meta-level abduction (2013)
  5. Finger, Marcelo: Towards automated first-order abduction: the cut-based approach (2012)
  6. Ma, Jiefei; Russo, Alessandra; Broda, Krysia; Lupu, Emil: Multi-agent confidential abductive reasoning (2011)
  7. Bourgne, Gauvain; Inoue, Katsumi; Maudet, Nicolas: Abduction of distributed theories through local interactions (2010)
  8. Inoue, Katsumi; Furukawa, Koichi; Kobayashi, Ikuo; Nabeshima, Hidetomo: Discovering rules by meta-level abduction (2010)
  9. Nabeshima, Hidetomo; Iwanuma, Koji; Inoue, Katsumi; Ray, Oliver: SOLAR: An automated deduction system for consequence finding (2010)
  10. Béreux, Natacha: Out-of-core implementations of Cholesky factorization: loop-based versus recursive algorithms (2008)
  11. Ray, Oliver; Inoue, Katsumi: Mode-directed inverse entailment for full clausal theories (2008)
  12. Inoue, Katsumi; Iwanuma, Koji; Nabeshima, Hidetomo: Consequence finding and computing answers with defaults (2006) ioport
  13. Inoue, Katsumi; Iwanuma, Koji; Nabeshima, Hidetomo: Consequence finding and computing answers with defaults (2006) ioport
  14. Bhatnagar, Arvind; Livingston, William: Fundamentals of solar astronomy. (2005)
  15. Nabeshima, Hidetomo; Iwanuma, Koji; Inoue, Katsumi: SOLAR: a consequence finding system for advanced reasoning (2003)
  16. Fahr, Hans J.; Scherer, Klaus: The adapted solar wind system as cause for a momentum transfer to the Sun and its consequences for the orbital motions of Keplerian objects (1993)