[](https://github.com/jsinger67/raa_tt/actions/workflows/rust.yml)
[](https://docs.rs/raa_tt)
[](https://crates.io/crates/raa_tt)
# 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](https://en.wikipedia.org/wiki/Method_of_analytic_tableaux) 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](https://en.wikipedia.org/wiki/Truth_table)
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](https://github.com/jsinger67/parol) parser
generator. The grammar used for propositions can be inspected
[here](https://github.com/jsinger67/raa_tt/blob/main/raa_tt.par). `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](https://github.com/jsinger67/raa_tt/blob/main/CHANGELOG.md)*
## How to use it?
Clone this repository and switch to the repository's folder.
Then run
```shell
cargo run ./test.txt
```
or
```shell
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:
```powershell
$env:RUST_LOG="raa_tt=trace,raa_tt::raa_tt_grammar_trait=error"
```
or
```powershell
$env:RUST_LOG="raa_tt=debug,raa_tt::raa_tt_grammar_trait=error"
```
## You found a bug?
Please, file an issue.