Computational Reasoners

The RAIR Lab is developing and/or using several computational reasoning systems:

  • SLATE [1], based on SRI’s SNARK, is a logic-based, robust interactive reasoning system that allows human “pilots” to harness an ensemble of intelligent agents in order to construct, test, and express various sorts of natural argumentation. It has been used extensively at RPI for teaching an introductory logic course.
  • TALOS (written in Python and based on SPASS) and ShadowProver (written in Lisp and based on SNARK) specify a natural deduction calculus for proving theorems in the cognitive calculus DCEC* [2]. Of these DCEC* provers, TALOS is available as a web-service, while ShadowProver is designed to be run locally.
  • OSCAR is an implementation of John Pollock’s non-monotonic defeasible reasoner.
  • MATR is a general purpose natural-deduction theorem prover for many logics.
  • SemanticProver is the implementation of two main theories of logic; the first being that of a semantic assignment, and the other being a metalogical framework to manipulate and reason about semantic assignments.
  • pyVivid [3] is an implementation of Arkoudas’ Vivid [4] framework for heterogenous diagrammatic-sentential reasoning in Python.
  • Microsoft Z3 [5] is a satisfiability modulo theories (SMT) solver created by Microsoft Research under the MIT license.
  • Athena [6] by Arkoudas, is a programming language and an interactive theorem proving environment rolled in one.
  • LEO-II & Satallax, systems for reasoning in the (higher-order) TPTP THF0 framework, which corresponds to Church’s simply typed lambda calculus with Henkin semantics.

References:

  1. S. Bringsjord and J. Taylor. Logic: A Modern Approach: Beginning Deductive Logic. Motalen, Troy, NY, 2015. This is an e-book edition of January 25 2016. The book is accompanied by the Slate software system, ISBN of 78-0-692-60734-3, and version of January 25 2016.
  2. Govindarajulu, Naveen Sundar, Selmer Bringsjord, and John Licato. “On deep computational formalization of natural language.” Proceedings of the Workshop:“Formalizing Mechanisms for Artificial General Intelligence and Cognition”(Formal MAGiC) at Artificial General Intelligence. 2013.
  3. N. Marton. PyVivid: A Concrete Framework for Mechanized Diagrammatic Reasoning. MS thesis, Rensselaer Polytechnic Institute (RPI), 2016.
  4. Arkoudas, Konstantine, and Selmer Bringsjord. “Vivid: A framework for heterogeneous problem solving.” Artificial Intelligence 173.15 (2009): 1367-1405.
  5. https://github.com/Z3Prover/z3
  6. http://proofcentral.org/athena/