raa_tt - Prover for sentences of propositional calculus

This crate provides an algorithm to decide whether a propositional formula is a tautology, a contradiction or contingent, i.e. its truth value depends on the truth values of its variables.

The algorithm used here is a form of Reductio ad absurdum, namely the truth tree method, a decision procedure for sentences of propositional logic. Especially for a larger number of logical variables this method is more efficient than other methods like e.g. truth tables

Essentially, the negation of the proposition is assumed to be true, and then raa_tt tries to refute that negated proposition, which indirectly proves that the original proposition is a tautology.

If this step did't succeed the algorithm is applied to the original (not negated) proposition. If this can be refuted the proposition is a contradiction, i.e. is always false independent from the values of its variables.

Otherwise the proposition is contingent.

To support users, the formula can be provided in textual form and is parsed by raa_tt binary tool. The input is parsed by a parser generated by parol parser generator. The grammar used for propositions can be inspected here. parol transformed it into a LL(1) grammar.

The parse result is later converted into a suitable representation [raa_tt::proposition::Proposition] that enables symbolic processing of the given propositional expression.

For latest changes please see CHANGELOG

How to use it?

Clone this repository and switch to the repository's folder.

Then run

cargo run ./test.txt

or

cargo run --release  ./test.txt

To test your own propositions, please modify the file test.txt.

Can you embed it into your own application?

Yes! raa_tt is a library, too. You can reference it in your own crate.

You want to explore the algorithm?

To support this you can use the logging feature.

Essentially set the RUST_LOG environment variable like in these examples which use the powershell:

$env:RUST_LOG="raa_tt=trace,raa_tt::raa_tt_grammar_trait=error"

or

$env:RUST_LOG="raa_tt=debug,raa_tt::raa_tt_grammar_trait=error"

You found a bug?

Please, file an issue.