raa_tt 0.9.1

Proves sentences of propositional calculus
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67

//! # RaaTT - Propositional Logic Prover
//!
//! A Rust crate for propositional logic reasoning and theorem proving for sentences of
//! propositional calculus using the analytic tableaux method (truth trees) and truth tables.
//! This library provides comprehensive support for logical operations, proposition handling, and
//! automated theorem proving.
//!
//! ## Features
//!
//! - **Logical Operators**: Support for all standard propositional logic operators including
//!   conjunction, disjunction, implication, bi-implication, and negation
//! - **Proposition System**: Flexible proposition representation and manipulation
//! - **Theorem Prover**: Automated reasoning engine for validating logical arguments
//! - **Truth Table Generation**: Comprehensive truth table construction and analysis
//! - **Grammar Parsing**: Built-in parser for logical expressions using the RaaTT grammar
//!
//! ## Example
//!
//! ```rust
//! use raa_tt::{
//!     prover::{Prover, ProveResult},
//!     proposition::Proposition,
//!     raa_tt_parser::parse,
//!     raa_tt_grammar::RaaTtGrammar,
//! };
//!
//! // Parse and prove a formula
//! let mut grammar = RaaTtGrammar::new();
//! parse("p -> (q -> p)", "example", &mut grammar).expect("Failed to parse");
//!
//! let proposition: Proposition = (&grammar.raa_tt.unwrap().raa_tt_list[0].biconditional).into();
//! let prover = Prover::new();
//! let result = prover.prove(&proposition).expect("Failed to prove");
//! match result {
//!     ProveResult::Proven => println!("Tautology: Always true"),
//!    ProveResult::Falsified => println!("Contradiction: Always false"),
//!    ProveResult::Contingent => println!("Contingent: Depends on variables"),
//!    _ => unreachable!(),
//! }
//! ```

/// Module with the BiImplication struct and its implementation.
pub mod bi_implication;
/// Module with the Conjunction struct and its implementation.
pub mod conjunction;
/// Module with the Disjunction struct and its implementation.
pub mod disjunction;
/// Module with the Errors enum and its implementation.
pub mod errors;
/// Module with the Implication struct and its implementation.
pub mod implication;
/// Module with the Negation struct and its implementation.
pub mod negation;
/// Module with the Proposition struct and its implementation.
pub mod proposition;
/// Module with the prover implementation.
pub mod prover;
/// Module with the RaaTTGrammar struct that provides the language processing.
pub mod raa_tt_grammar;
/// Module with the RaaTTGrammarTrait trait generated by Parol.
mod raa_tt_grammar_trait;
/// Module with the RaaTtParser struct generated by Parol.
pub mod raa_tt_parser;
/// Module with the table generator functionality.
pub mod table_generator;
/// Module with the TruthTable struct and its implementation.
pub mod truth_table;