Aris

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.

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 main folders of interest for our project are the following:

• proof-client - Contains the client side module of the Aris Proof system (essentially, this is the frontend). proof-client calls libaris; libaris is the underlying logic engine.
• libaris - Contains a logic software library used by Aris Proof (essentially, this is the backend). The Rust code which powers the logic backend is contained here.

The main code which deals with implementing first order logic is contained within https://github.com/Bram-Hub/Aris/tree/master/libaris/src/main/java/edu/rpi/aris

The rules used for first order logic proofs appear to be defined in https://github.com/Bram-Hub/Aris/blob/master/libaris/src/main/rust/src/rules.rs .

Also of note: Aris contains code to convert a sentence string into Polish notation: https://github.com/Bram-Hub/Aris/blob/master/libaris/src/main/java/edu/rpi/aris/proof/SentenceUtil.java . Perhaps this will help us with the shunting yard algorithm? However, in Aris, the polish notation has been deprecated in favor of parsing into an expression tree defined in https://github.com/BramHub/Aris/blob/c3bb0ed21191ee552f60a3c306f0df1870f8b8b0/libaris/src/main/rust/src/expression.rs#L25-L34 .

WIP....