Aris

Introduction

Aris is a tool created by students working under Professor Bram van Heuveln at Rensselaer Polytechnic Institute for evaluating first order logic proofs. This application could be useful to study in order to help us implement first order logic into ALPACA.

Findings

The code for Aris is located at https://github.com/Bram-Hub/Aris and is written in a combination of Java and Rust (frontend is in Java, backend is in Java and Rust). The project has two components: a server (which contains the logic of the program), and a client (for interacting with the server).

The file that handles the logic of verifying various first order logic rules (such as or elimination, and introduction, etc) are at https://github.com/Bram-Hub/aris/blob/master/src/rules.rs. Most of the logic for rule checking starts at line 334. The function at line 661 contains more rules for handling quanitifers.

Expressions are represented using a Rust enum at https://github.com/Bram-Hub/aris/blob/master/src/expression.rs. This allows Expressions to represent contradition, tautology, or expressions using unary, binary, and associative operators, as well as quantifiers.

What isn't so helpful

In the end, after studying the Aris code, I have come to the conclusion that, while it might be useful for reference as we build inference rules into ALPACA, we may not want to use it at all. There are two reasons for this:

1. The Aris code doesn't do anything special; it is exactly what you would expect. For instance, if you have A ^ B ^ C and do an AND ELIM to isolate C, it just verifies that C is one of the expressions in the original conjunction, which is literally just the definition of AND ELIM. In short, the code isn't doing any special tricks, it's just simply implementing the rules as you would expect. While we could study the Aris code for tips when we are unsure of the best way to implement an inference rule in ALPACA, I don't believe this will really be necessary, as we can simply use our intuition and build these rules into ALPACA from scratch very easily.
2. Aris is written in Rust, and nobody on our team understands Rust, which makes it difficult to understand how Aris's first order logic system works, much less implement something based on it into ALPACA.

What is helpful

There are a few things in the code that could be of use. For instance, in rules.rs, the following note is made regarding how to verify Existential Elimination: ` /* 1 | exists x, phi(x) | --- 2 | | phi(a) | | --- 3 | | psi, SomeRule, 2 4 | psi, ExistElim, 2-3

• the body of the existential in dep 1 must unify with the premise of the subproof at 2, this infers the skolem constant
• the conclusion 4 must occur in some line of the subproof at 2-3 (in this, 3)
• the skolem constant must not occur in the transitive dependencies of the conclusion (generalizable variable conterexample check)
• the skolem constant must not escape to the conclusion (freevars check) */`

This essentially gives us a list 4 things we must check for in order for existential elimination to be valid. We could check for these 4 things in ALPACA when coding our existential elimination rule.

We also get a glimpse of the syntax for constructing a proof in Aris:

Creating a proof programatically

ASCII art proof:

1 | P -> Q
  | ---
2 | | ~Q
  | | ---
3 | | | P
  | | | ---
4 | | | Q ; ImpElim, [1, 3]
5 | | | _|_ ; ContradictionIntro, [2, 4]
6 | | ~P ; NotIntro, [3..5]
7 | ~Q -> ~P ; ImpIntro [2..6]

Code that builds the proof generically and then instantiates it:

#[macro_use] extern crate frunk;
use libaris::expression::Expr;
use libaris::proofs::{Proof, Justification, pooledproof::PooledProof};
use libaris::rules::RuleM;
fn contraposition_demo<P: Proof>() -> P {
    use libaris::parser::parse_unwrap as p;
    let mut prf = P::new();
    let line1 = prf.add_premise(p("P -> Q"));
    let sub2to6 = prf.add_subproof();
    prf.with_mut_subproof(&sub2to6, |sub1| {
        let line2 = sub1.add_premise(p("~Q"));
        let sub3to5 = sub1.add_subproof();
        sub1.with_mut_subproof(&sub3to5, |sub2| {
            let line3 = sub2.add_premise(p("P"));
            let line4 = sub2.add_step(Justification(p("Q"), RuleM::ImpElim, vec![line1.clone(), line3.clone()], vec![]));
            let line5 = sub2.add_step(Justification(p("_|_"), RuleM::ContradictionIntro, vec![line2.clone(), line4.clone()], vec![]));
        }).unwrap();
        let line6 = sub1.add_step(Justification(p("~P"), RuleM::NotIntro, vec![], vec![sub3to5]));
    }).unwrap();
    let line7 = prf.add_step(Justification(p("~Q -> ~P"), RuleM::ImpIntro, vec![], vec![sub2to6]));
    prf
}
`