oxilean_std/logic/
types.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use super::functions::*;
6use oxilean_kernel::{BinderInfo, Declaration, Environment, Expr, Level, Name};
7
8/// Represents a proof system and its complexity measures.
9#[allow(dead_code)]
10#[derive(Debug, Clone)]
11pub struct ProofComplexitySystem {
12    /// Name of the proof system.
13    pub name: String,
14    /// Whether the system has polynomial-size proofs for tautologies (p-simulation).
15    pub has_p_simulations: bool,
16    /// Whether the system can simulate resolution.
17    pub simulates_resolution: bool,
18    /// The Cook-Reckhow conjectured lower bound on proof size.
19    pub super_polynomial_lower_bound: bool,
20}
21#[allow(dead_code)]
22impl ProofComplexitySystem {
23    /// Create a new proof complexity system descriptor.
24    pub fn new(name: &str) -> Self {
25        ProofComplexitySystem {
26            name: name.to_string(),
27            has_p_simulations: false,
28            simulates_resolution: false,
29            super_polynomial_lower_bound: false,
30        }
31    }
32    /// Resolution proof system.
33    pub fn resolution() -> Self {
34        let mut sys = ProofComplexitySystem::new("Resolution");
35        sys.simulates_resolution = true;
36        sys
37    }
38    /// Extended Frege system.
39    pub fn extended_frege() -> Self {
40        let mut sys = ProofComplexitySystem::new("Extended Frege");
41        sys.has_p_simulations = true;
42        sys.simulates_resolution = true;
43        sys
44    }
45    /// Frege system (Hilbert-style).
46    pub fn frege() -> Self {
47        let mut sys = ProofComplexitySystem::new("Frege");
48        sys.simulates_resolution = true;
49        sys
50    }
51    /// Cook-Reckhow theorem: if NP ≠ coNP, no proof system is polynomially bounded.
52    pub fn cook_reckhow_separation(&self) -> bool {
53        true
54    }
55    /// Propositional pigeonhole principle: known to require exponential proofs in Resolution.
56    pub fn php_complexity(&self) -> String {
57        match self.name.as_str() {
58            "Resolution" => "Exponential lower bound (Ben-Sasson-Wigderson 2001)".to_string(),
59            "Extended Frege" => "Polynomial upper bound".to_string(),
60            _ => "Unknown".to_string(),
61        }
62    }
63}
64/// A truth value in a many-valued logic.
65#[allow(dead_code)]
66#[derive(Debug, Clone, PartialEq)]
67pub enum ManyValuedTruth {
68    /// True.
69    True,
70    /// False.
71    False,
72    /// Both true and false (glutted).
73    Both,
74    /// Neither true nor false (gapped).
75    Neither,
76    /// A numerical value in [0, 1] (fuzzy).
77    Fuzzy(f64),
78}
79#[allow(dead_code)]
80impl ManyValuedTruth {
81    /// Is this value "designated" (true-like) in LP/FDE.
82    pub fn is_designated(&self) -> bool {
83        matches!(self, ManyValuedTruth::True | ManyValuedTruth::Both)
84    }
85    /// Kleene three-valued conjunction: A ∧ B.
86    pub fn kleene_and(a: &ManyValuedTruth, b: &ManyValuedTruth) -> ManyValuedTruth {
87        use ManyValuedTruth::*;
88        match (a, b) {
89            (True, True) => True,
90            (False, _) | (_, False) => False,
91            (Neither, _) | (_, Neither) => Neither,
92            _ => Both,
93        }
94    }
95    /// Kleene three-valued disjunction: A ∨ B.
96    pub fn kleene_or(a: &ManyValuedTruth, b: &ManyValuedTruth) -> ManyValuedTruth {
97        use ManyValuedTruth::*;
98        match (a, b) {
99            (False, False) => False,
100            (True, _) | (_, True) => True,
101            (Neither, _) | (_, Neither) => Neither,
102            _ => Both,
103        }
104    }
105    /// Kleene three-valued negation: ¬A.
106    pub fn kleene_not(a: &ManyValuedTruth) -> ManyValuedTruth {
107        use ManyValuedTruth::*;
108        match a {
109            True => False,
110            False => True,
111            Neither => Neither,
112            Both => Both,
113            Fuzzy(v) => Fuzzy(1.0 - v),
114        }
115    }
116}
117/// Describes a second-order logic system.
118#[allow(dead_code)]
119#[derive(Debug, Clone)]
120pub struct SecondOrderLogic {
121    /// Whether comprehension axiom is full or restricted.
122    pub full_comprehension: bool,
123    /// Whether the system includes induction.
124    pub with_induction: bool,
125    /// The second-order system name.
126    pub system_name: String,
127}
128#[allow(dead_code)]
129impl SecondOrderLogic {
130    /// Create a new second-order logic descriptor.
131    pub fn new(system_name: &str, full_comprehension: bool, with_induction: bool) -> Self {
132        SecondOrderLogic {
133            full_comprehension,
134            with_induction,
135            system_name: system_name.to_string(),
136        }
137    }
138    /// Second-order arithmetic Z_2 (full second-order arithmetic).
139    pub fn z2() -> Self {
140        SecondOrderLogic::new("Z_2", true, true)
141    }
142    /// ACA_0: Arithmetical Comprehension Axiom (base system of second-order arithmetic).
143    pub fn aca0() -> Self {
144        SecondOrderLogic::new("ACA_0", false, true)
145    }
146    /// Whether this system interprets first-order PA (Peano Arithmetic).
147    pub fn interprets_pa(&self) -> bool {
148        self.with_induction && !self.full_comprehension || self.full_comprehension
149    }
150    /// Categoricity: second-order PA is categorical (all models are isomorphic).
151    pub fn is_categorical(&self) -> bool {
152        self.full_comprehension
153    }
154    /// Incompleteness: by Gödel, Z_2 is incomplete if ω-consistent.
155    pub fn is_complete(&self) -> bool {
156        false
157    }
158}
159/// Sequent calculus proof tree.
160#[allow(dead_code)]
161#[derive(Debug, Clone)]
162pub struct SequentProof {
163    pub antecedents: Vec<String>,
164    pub consequent: String,
165    pub rule_name: String,
166    pub premises: Vec<SequentProof>,
167}
168#[allow(dead_code)]
169impl SequentProof {
170    pub fn axiom(formula: &str) -> Self {
171        SequentProof {
172            antecedents: vec![formula.to_string()],
173            consequent: formula.to_string(),
174            rule_name: "Ax".to_string(),
175            premises: Vec::new(),
176        }
177    }
178    pub fn new(ants: Vec<&str>, cons: &str, rule: &str, prems: Vec<SequentProof>) -> Self {
179        SequentProof {
180            antecedents: ants.iter().map(|s| s.to_string()).collect(),
181            consequent: cons.to_string(),
182            rule_name: rule.to_string(),
183            premises: prems,
184        }
185    }
186    pub fn height(&self) -> usize {
187        if self.premises.is_empty() {
188            0
189        } else {
190            1 + self.premises.iter().map(|p| p.height()).max().unwrap_or(0)
191        }
192    }
193    pub fn n_leaves(&self) -> usize {
194        if self.premises.is_empty() {
195            1
196        } else {
197            self.premises.iter().map(|p| p.n_leaves()).sum()
198        }
199    }
200}
201/// Linear temporal logic (LTL) formula.
202#[allow(dead_code)]
203#[derive(Debug, Clone)]
204pub enum LTLFormula {
205    Atom(String),
206    Not(Box<LTLFormula>),
207    And(Box<LTLFormula>, Box<LTLFormula>),
208    Or(Box<LTLFormula>, Box<LTLFormula>),
209    Next(Box<LTLFormula>),
210    Globally(Box<LTLFormula>),
211    Finally(Box<LTLFormula>),
212    Until(Box<LTLFormula>, Box<LTLFormula>),
213}
214#[allow(dead_code)]
215impl LTLFormula {
216    pub fn atom(s: &str) -> Self {
217        LTLFormula::Atom(s.to_string())
218    }
219    pub fn safety(phi: LTLFormula) -> Self {
220        LTLFormula::Globally(Box::new(phi))
221    }
222    pub fn liveness(phi: LTLFormula) -> Self {
223        LTLFormula::Finally(Box::new(phi))
224    }
225    pub fn is_temporal(&self) -> bool {
226        matches!(
227            self,
228            LTLFormula::Next(_)
229                | LTLFormula::Globally(_)
230                | LTLFormula::Finally(_)
231                | LTLFormula::Until(_, _)
232        )
233    }
234    pub fn depth(&self) -> usize {
235        match self {
236            LTLFormula::Atom(_) => 0,
237            LTLFormula::Not(f) => 1 + f.depth(),
238            LTLFormula::And(f, g) | LTLFormula::Or(f, g) | LTLFormula::Until(f, g) => {
239                1 + f.depth().max(g.depth())
240            }
241            LTLFormula::Next(f) | LTLFormula::Globally(f) | LTLFormula::Finally(f) => 1 + f.depth(),
242        }
243    }
244}
245/// Modal logic Kripke frame.
246#[allow(dead_code)]
247#[derive(Debug, Clone)]
248pub struct KripkeFrame {
249    pub worlds: Vec<String>,
250    pub accessibility: Vec<(usize, usize)>,
251}
252#[allow(dead_code)]
253impl KripkeFrame {
254    pub fn new(worlds: Vec<&str>) -> Self {
255        KripkeFrame {
256            worlds: worlds.iter().map(|s| s.to_string()).collect(),
257            accessibility: Vec::new(),
258        }
259    }
260    pub fn add_access(&mut self, w: usize, v: usize) {
261        self.accessibility.push((w, v));
262    }
263    pub fn is_reflexive(&self) -> bool {
264        (0..self.worlds.len()).all(|w| self.accessibility.contains(&(w, w)))
265    }
266    pub fn is_transitive(&self) -> bool {
267        for &(w, v) in &self.accessibility {
268            for &(v2, u) in &self.accessibility {
269                if v == v2 && !self.accessibility.contains(&(w, u)) {
270                    return false;
271                }
272            }
273        }
274        true
275    }
276    pub fn is_symmetric(&self) -> bool {
277        self.accessibility
278            .iter()
279            .all(|&(w, v)| self.accessibility.contains(&(v, w)))
280    }
281    pub fn modal_logic_name(&self) -> &'static str {
282        match (
283            self.is_reflexive(),
284            self.is_transitive(),
285            self.is_symmetric(),
286        ) {
287            (true, true, true) => "S5 (equivalence relation)",
288            (true, true, false) => "S4",
289            (true, false, false) => "T",
290            (false, true, false) => "K4",
291            _ => "K (basic modal logic)",
292        }
293    }
294}
295/// Represents a paraconsistent logic: a logic where contradictions do not
296/// cause explosion (ex falso quodlibet fails).
297#[allow(dead_code)]
298#[derive(Debug, Clone, PartialEq)]
299pub enum ParaconsistentSystem {
300    /// LP (Logic of Paradox): allows true contradictions (dialetheism).
301    LP,
302    /// FDE (First Degree Entailment): four-valued logic.
303    FDE,
304    /// Relevant logic R.
305    RelevantR,
306    /// Priest's LP with modus ponens.
307    PriestLP,
308    /// Jaskowski's discussive logic D2.
309    JaskowskiD2,
310}
311#[allow(dead_code)]
312impl ParaconsistentSystem {
313    /// Returns the number of truth values in the system.
314    pub fn num_truth_values(&self) -> usize {
315        match self {
316            ParaconsistentSystem::LP => 3,
317            ParaconsistentSystem::FDE => 4,
318            ParaconsistentSystem::RelevantR => 2,
319            ParaconsistentSystem::PriestLP => 3,
320            ParaconsistentSystem::JaskowskiD2 => 2,
321        }
322    }
323    /// Check if the law of explosion (⊢ A → (¬A → B)) holds.
324    pub fn explosion_holds(&self) -> bool {
325        match self {
326            ParaconsistentSystem::LP => false,
327            ParaconsistentSystem::FDE => false,
328            ParaconsistentSystem::RelevantR => false,
329            ParaconsistentSystem::PriestLP => false,
330            ParaconsistentSystem::JaskowskiD2 => false,
331        }
332    }
333    /// Whether this system handles the liar paradox consistently.
334    pub fn handles_liar_paradox(&self) -> bool {
335        match self {
336            ParaconsistentSystem::LP => true,
337            ParaconsistentSystem::FDE => true,
338            _ => false,
339        }
340    }
341}
oxilean_std/logic/types.rs

oxilean_std/logic/
types.rs
