7 lines
405 B
Plaintext
7 lines
405 B
Plaintext
GNU Aris is a sequential proof program, designed to assist anyone
|
|
interested in solving logical proofs. Aris supports both propositional
|
|
and predicate logic, as well as Boolean algebra and arithmetical logic
|
|
in the form of abstract sequences. It uses a predefined set of both
|
|
inference and equivalence rules, however gives the user options to use
|
|
older proofs as lemmas, including Isabelle's Isar proofs.
|