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.
|