NOTE: This page serves as an archive for the development of MATR at the RAIR Lab. MATR is currently being developed at the AMHR Lab at USF, with more information coming soon!

Machina Arachne Tree-Based Reasoner (M.A.T*R or simply MATR) is a fast, extensible, and parallelized natural deduction theorem prover.

MATR uses natural deduction to prove theorems. It treats formulas as tree-based symbols that can be manipulated using certain rules. MATR is given input axiom formulas and rules that it can apply to those symbols, then MATR uses these rules to prove new formulas in an attempt to prove the desired conclusions. Using natural deduction allows MATR to support higher order logic, deontic logic, many-sorted logic, situational logic, numeric logic, and most other logics not mentioned while still providing concise and readable proofs when finished.

MATR is fast because it represents logical formulas as trees of sub-formulas. This allows for efficient pattern matching and search while efficient interning of formulas reduces memory costs. Furthermore, MATR is written in Java: one of the fastest modern programming languages and reaps great benefits of the JVM’s self optimizing runtime.

MATR is parallelized because of its codelet architecture. Codelets are the implementations of various logical rules and proof tactics. Codelets can be big or small: anything from a rule codelet that just adds simple derivations, to a prover codelet that contains a whole theorem prover and adds entire chunks of derivations at a time. Due to their independent and self contained design all codelets are run simultaneously. In addition, MATR optimizes which Codelets are run on which parts of the proof and prioritizes those that are deriving useful results.

MATR is extensible because of the combination of these three properties. Firstly the speed of MATR makes it worthwhile to extend in the first place. Secondly, MATR’s natural deduction framework makes it possible to extend MATR with any type of logic, no matter how bizarre. Finally, adding functionality is as easy as making a new codelet, and the self contained design of codelets allows them to be run at the same time on the same problem and not have to worry about compatibility issues.

Once MATR reaches a stable release it will be coming to a github near you!