SOLAR swMATH ID: 888 Software Authors: Hidetomo Nabeshima, Koji Iwanuma, Katsumi Inoue, Oliver Ray Description: 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. Homepage: http://dl.acm.org/citation.cfm?id=1735932 Keywords: Consequence finding; theorem proving; SOL calculus; connection tableaux; first-order logic Related Software: E Theorem Prover; SPASS; SCIFF; MiniSat; SBGN; SMT-LIB; TPTP; TopLog; ELK; DeepProbLog; PRISM; cplint; PrASP; XSB; CP-logic; ProbLog; CVC4; z3; VAMPIRE; clasp Cited in: 19 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year SOLAR: An automated deduction system for consequence finding. Zbl 1205.68362Nabeshima, Hidetomo; Iwanuma, Koji; Inoue, Katsumi; Ray, Oliver 2010 all top 5 Cited by 44 Authors 7 Inoue, Katsumi 5 Nabeshima, Hidetomo 3 Iwanuma, Koji 2 Demolombe, Robert 2 Echenim, Mnacho 2 Fariñas del Cerro, Luis 2 Obeid, Naji 2 Peltier, Nicolas 2 Ray, Oliver 2 Tourret, Sophie 1 Alliot, Jean-Marc 1 Azzolini, Damiano 1 Bellodi, Elena 1 Béreux, Natacha 1 Bhatnagar, Arvind 1 Bourgne, Gauvain 1 Broda, Krysia B. 1 Diéguez, Martín 1 Doncescu, Andrei 1 Fahr, Hans J. 1 Ferilli, Stefano 1 Finger, Marcelo 1 Froidevaux, Christine 1 Furukawa, Kōichi 1 Haifani, Fajar 1 Kobayashi, Ikuo 1 Koopmann, Patrick 1 Lin, Dianhuan 1 Livingston, William 1 Lupu, Emil 1 Ma, Jiefei 1 Maudet, Nicolas 1 Moriya, Hisao 1 Muggleton, Stephen H. 1 Pahlavi, Niels 1 Riguzzi, Fabrizio 1 Rougny, Adrien 1 Russo, Alessandra M. 1 Scherer, Klaus R. 1 Sellami, Yanis 1 Tamaddoni-Nezhad, Alireza 1 Weidenbach, Christoph 1 Yamamoto, Yoshitaka 1 Zese, Riccardo all top 5 Cited in 8 Serials 2 Machine Learning 1 Astrophysics and Space Science 1 International Journal of Approximate Reasoning 1 SIAM Journal on Matrix Analysis and Applications 1 AI Communications 1 Logic Journal of the IGPL 1 Journal of Applied Logic 1 World Scientific Series in Astronomy and Astrophysics all top 5 Cited in 7 Fields 15 Computer science (68-XX) 4 Mathematical logic and foundations (03-XX) 3 Biology and other natural sciences (92-XX) 2 Astronomy and astrophysics (85-XX) 1 Numerical analysis (65-XX) 1 Mechanics of particles and systems (70-XX) 1 Fluid mechanics (76-XX) Citations by Year