This program takes string formulas or DIMACS files as an input and can produce parse trees, resolution proofs and DPLL proofs.
Input can be given either as a string based formula, or as a DIMACS formatted file. These will then be parsed into an abstract syntax tree which is then reduced to conjunctive normal form.
A resolution proof is completed by negating the given formula, this negation is then fully resolved to determine it's satisfiability and the original formulas validity is set.
A DPLL proof will determine whether or not a given formula is satisfiable or not, giving a model if it is satisfiable.
unzip the reasoning_1522968.zip file into the desired directory. Now run
./build
in order to build the program for use (note: this may require admin privileges). See the section below for details of how to run the program.
The program can be built from source using the build script:
./build
Once built the program can be run using the running script:
./run [<flag> [args]*]*
Examples can be found below. The program is also test-driven, there are currently test files for DPLL proofs, Resolution Proofs, the DIMACS parser and clauses. To run the tests, use the test suite.
./run -f "(((A->B)&(B->C))->(A->C))"
Will output resolution and DPLL proofs of transitivity.
./run -f "((-(A+B))->((-A)&(-B)))" -o "out.txt" -v
Will output resolution and DPLL proofs of transitivity whilst providing a verbose output in "out.txt".
./run -d "DIMACSTestFiles/dimacs1.txt" -o "out.txt" -v
Will output resolution and DPLL proofs from the contents of "DIMACSTestFiles/dimacs1.txt" whilst providing verbose output in "out.txt".