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

For easy use, the formula can be provided in textual form and is parsed by raa_tt binary tool. The grammar used for propositions can be inspected here.

For latest changes please see CHANGELOG

How to use it?

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

Then run, e.g.

cargo run -- -f ./test.txt
cargo run --release -- -s "((p -> q) & (r -> s) & (p | r)) -> q | s"

Alternatively you can install raa_tt via

cargo install raa_tt

Then you can call it directly from the command line, e.g. like

raa_tt -s "(a & a -> b) -> b" -q

You can use command line argument -h to get help.

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.