theorem_prover/
lib.rs

1//! # Theorem Prover for First-Order Logic
2//!
3//! `theorem_prover` provides utilities to create formulas and pass them to `is_valid`
4//! to decide if the given formula is valid.
5
6use lang::{Formula, Term};
7use log::trace;
8use std::collections::HashMap;
9
10mod clausal;
11pub mod lang;
12mod resolution;
13mod unification;
14
15type Arity = HashMap<String, usize>;
16
17#[derive(Debug, PartialEq)]
18pub enum ProverError {
19    ArityError,
20    TimeoutError,
21}
22
23/// Check if a given formula is valid
24///
25/// Must pass a time limit in seconds to avoid infinite loops (default is 60)
26///
27/// # Example
28///
29/// ```
30/// use theorem_prover::{lang::{Formula, Pred, Term, Var}, ProverError, Imply, Exists, Forall, Pred, Var};
31/// let formula = Imply!(
32///     Exists!("x", Pred!("p", [Var!("x")])),
33///     Forall!("x", Pred!("p", [Var!("x")]))
34/// );
35/// ```
36///
37/// `is_valid(formula, 5).unwrap()` will evaluate to `false`
38///
39pub fn is_valid(formula: Formula, limit_in_seconds: u64) -> Result<bool, ProverError> {
40    if !check_arity(&formula) {
41        return Err(ProverError::ArityError);
42    }
43    trace!("Negating {formula}");
44    let negated = Formula::Neg(Box::new(formula));
45    let clausal = clausal::to_clausal(negated);
46    resolution::refute_resolution(clausal, limit_in_seconds)
47}
48
49fn check_arity(formula: &Formula) -> bool {
50    let mut pred_arity = HashMap::new();
51    let mut func_arity = HashMap::new();
52    check_arity_in_formula(formula, &mut pred_arity, &mut func_arity)
53}
54
55fn check_arity_in_formula(
56    formula: &Formula,
57    pred_arity: &mut Arity,
58    func_arity: &mut Arity,
59) -> bool {
60    match formula {
61        Formula::Pred(pred) => {
62            if let Some(arity) = pred_arity.get(pred.get_id()) {
63                if arity != &pred.get_args().len() {
64                    return false;
65                }
66            } else {
67                pred_arity.insert(pred.get_id().to_string(), pred.get_args().len());
68            }
69            pred.get_args()
70                .iter()
71                .all(|arg| check_arity_in_term(arg, pred_arity, func_arity))
72        }
73        Formula::True => true,
74        Formula::False => true,
75        Formula::And(left, right) => {
76            check_arity_in_formula(left, pred_arity, func_arity)
77                && check_arity_in_formula(right, pred_arity, func_arity)
78        }
79        Formula::Or(left, right) => {
80            check_arity_in_formula(left, pred_arity, func_arity)
81                && check_arity_in_formula(right, pred_arity, func_arity)
82        }
83        Formula::Neg(subformula) => check_arity_in_formula(subformula, pred_arity, func_arity),
84        Formula::Imply(left, right) => {
85            check_arity_in_formula(left, pred_arity, func_arity)
86                && check_arity_in_formula(right, pred_arity, func_arity)
87        }
88        Formula::Iff(left, right) => {
89            check_arity_in_formula(left, pred_arity, func_arity)
90                && check_arity_in_formula(right, pred_arity, func_arity)
91        }
92        Formula::Forall(_, subformula) => {
93            check_arity_in_formula(subformula, pred_arity, func_arity)
94        }
95        Formula::Exists(_, subformula) => {
96            check_arity_in_formula(subformula, pred_arity, func_arity)
97        }
98    }
99}
100
101fn check_arity_in_term(term: &Term, pred_arity: &mut Arity, func_arity: &mut Arity) -> bool {
102    match term {
103        Term::Obj(_) => true,
104        Term::Var(_) => true,
105        Term::Fun(f) => {
106            if let Some(arity) = func_arity.get(f.get_id()) {
107                if arity != &f.get_args().len() {
108                    return false;
109                }
110            } else {
111                func_arity.insert(f.get_id().to_string(), f.get_args().len());
112            }
113            f.get_args()
114                .iter()
115                .all(|arg| check_arity_in_term(arg, pred_arity, func_arity))
116        }
117    }
118}
119
120#[cfg(test)]
121mod tests {
122    use super::*;
123    use crate::lang::{Pred, Term, Var};
124
125    const DEFAULT_LIMIT: u64 = 60;
126
127    #[test]
128    fn test_valid_formula() {
129        let formula = Neg!(Exists!(
130            "y",
131            Forall!(
132                "z",
133                Iff!(
134                    Pred!("p", [Var!("z"), Var!("y")]),
135                    Neg!(Exists!(
136                        "x",
137                        And!(
138                            Pred!("p", [Var!("z"), Var!("x")]),
139                            Pred!("p", [Var!("x"), Var!("z")])
140                        )
141                    ))
142                )
143            )
144        )); // F : ~(exists y.(forall z.((p(z, y)) <-> (~(exists x.((p(z, x)) /\ (p(x, z))))))))
145        assert!(is_valid(formula, DEFAULT_LIMIT).unwrap());
146    }
147
148    #[test]
149    fn test_invalid_formula() {
150        let formula = Imply!(
151            Exists!("x", Pred!("p", [Var!("x")])),
152            Forall!("x", Pred!("p", [Var!("x")]))
153        ); // F : exists x.(p(x)) -> forall x.(p(x))
154        assert!(!is_valid(formula, DEFAULT_LIMIT).unwrap());
155    }
156
157    #[test]
158    fn test_unknown_formula() {
159        let formula = Neg!(Forall!(
160            "x",
161            Forall!(
162                "y",
163                And!(
164                    Or!(Pred!("p", [Var!("x")]), Neg!(Pred!("q", [Var!("x")]))),
165                    Or!(Neg!(Pred!("p", [Var!("y")])), Pred!("q", [Var!("y")]))
166                )
167            )
168        )); // F: ~(forall x.(forall y.((p(x) \/ ~q(x)) /\ (~p(y) \/ q(y)))))
169        assert!(is_valid(formula, 5) == Err(ProverError::TimeoutError));
170    }
171}
theorem_prover/lib.rs

theorem_prover/
lib.rs
