6 releases (breaking)
0.5.0 | Sep 19, 2024 |
---|---|
0.4.1 | Feb 13, 2024 |
0.4.0 | Nov 9, 2023 |
0.3.0 | Nov 5, 2023 |
0.1.0 | Nov 1, 2023 |
#274 in Math
239 downloads per month
88KB
2K
SLoC
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.
Dependencies
~7–17MB
~184K SLoC