System Larus

Larus

People

• Predrag Janičić
• Julien Narboux

Short Description

Larus is a theorem prover for coherent logic that uses SAT/SMT provers to construct proofs. Larus can generate natural language proofs (in LaTeX) and verifiable Coq proofs.

Capabilities

• Proving
• Model finding

Input Language

The input format is TPTP/Fol restricted to formulas which are in coherent logic form. The formulas should not use any function symbol, only predicate symbols are supported.

Output

The output is displayed using TPTP SZS ontology.

If a proof is found Larus will output: % SZS status Theorem otherwise: % SZS status Unknown

Proof Format

Proofs can be exported either using Latex or using Coq's language. The output is designed to obtain proofs which are human readable. The proofs are presented in a forward reasoning style.

Official Page

Larus

Other relevant information

This software is distributed under the licence GPLv3.

Status

Research prototype. Maintained

References

Predrag Janicic, Julien Narboux. Theorem Proving as Constraint Solving with Coherent Logic. Journal of Automated Reasoning, 66, pages 689–746 (2022), ⟨10.1007/s10817-022-09629-z⟩

Tools

Larus can use the following external tools :

• URSA (http://www.matf.bg.ac.rs/~janicic/software/ursa.zip)
• Z3 (https://github.com/Z3Prover/z3)
• Vampire (https://vprover.github.io/)
• Coq (https://coq.inria.fr/)