oxilean_std/proof_mining/
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#[allow(dead_code)]
9#[derive(Debug, Clone)]
10pub struct DialecticaInterp {
11    pub formula: String,
12    pub witness_type: String,
13    pub counterexample_type: String,
14    pub is_godel_dialectica: bool,
15}
16#[allow(dead_code)]
17impl DialecticaInterp {
18    pub fn new(formula: &str, witness: &str, counter: &str) -> Self {
19        DialecticaInterp {
20            formula: formula.to_string(),
21            witness_type: witness.to_string(),
22            counterexample_type: counter.to_string(),
23            is_godel_dialectica: true,
24        }
25    }
26    pub fn godel_t_translation(&self) -> String {
27        format!(
28            "Dialectica: '{}' → ∃{}.∀{}.A({}, {})",
29            self.formula,
30            self.witness_type,
31            self.counterexample_type,
32            self.witness_type,
33            self.counterexample_type
34        )
35    }
36    pub fn modified_realizability(&self) -> String {
37        format!(
38            "Modified realizability of '{}': witness type = {}",
39            self.formula, self.witness_type
40        )
41    }
42    pub fn soundness_theorem(&self) -> String {
43        "Dialectica interpretation is sound for Heyting arithmetic + AC_qf + IPP".to_string()
44    }
45    pub fn is_sound_for_classical(&self) -> bool {
46        true
47    }
48}
49/// G_del functional interpretation.
50#[allow(dead_code)]
51#[derive(Debug, Clone)]
52pub struct GodelInterpretation {
53    pub theorem: String,
54    pub functional_type: String,
55    pub realizing_term: String,
56}
57impl GodelInterpretation {
58    #[allow(dead_code)]
59    pub fn new(thm: &str, ftype: &str, term: &str) -> Self {
60        Self {
61            theorem: thm.to_string(),
62            functional_type: ftype.to_string(),
63            realizing_term: term.to_string(),
64        }
65    }
66    #[allow(dead_code)]
67    pub fn soundness_statement(&self) -> String {
68        format!("If HA proves A, then T proves A^D where A^D is the Dialectica interpretation",)
69    }
70}
71/// The empty clause ⊥ (proof of contradiction).
72#[derive(Debug, Clone)]
73pub struct EmptyClause;
74impl EmptyClause {
75    /// Return the empty clause.
76    pub fn as_clause() -> Clause {
77        Clause::empty()
78    }
79}
80/// Proof-as-program correspondence (Curry-Howard).
81#[derive(Debug, Clone)]
82pub struct CurryHoward {
83    /// The proposition (as a string).
84    pub proposition: String,
85    /// The corresponding type (as a string).
86    pub corresponding_type: String,
87}
88impl CurryHoward {
89    /// Create a new Curry-Howard correspondence entry.
90    pub fn new(proposition: impl Into<String>, corresponding_type: impl Into<String>) -> Self {
91        Self {
92            proposition: proposition.into(),
93            corresponding_type: corresponding_type.into(),
94        }
95    }
96    /// Return a human-readable summary.
97    pub fn describe(&self) -> String {
98        format!(
99            "Prop: {} <-> Type: {}",
100            self.proposition, self.corresponding_type
101        )
102    }
103}
104/// Checks Howard/Bezem majorizability for a pair of functions (represented as tables).
105#[derive(Debug, Clone)]
106pub struct MajorizabilityChecker {
107    /// Values of the "major" function f (f(i) at index i).
108    pub f_values: Vec<u64>,
109    /// Values of the "minor" function g (g(i) at index i).
110    pub g_values: Vec<u64>,
111}
112impl MajorizabilityChecker {
113    /// Create a checker for f majorizing g (both given as value tables).
114    pub fn new(f_values: Vec<u64>, g_values: Vec<u64>) -> Self {
115        Self { f_values, g_values }
116    }
117    /// Returns true if f Howard-majorizes g: ∀n, g(n) ≤ f(n).
118    pub fn howard_majorizes(&self) -> bool {
119        self.f_values
120            .iter()
121            .zip(self.g_values.iter())
122            .all(|(&fv, &gv)| gv <= fv)
123    }
124    /// Returns true if f Bezem-majorizes g:
125    /// ∀m ≤ n, g(m) ≤ f(n) (strong majorizability).
126    pub fn bezem_majorizes(&self) -> bool {
127        let n = self.f_values.len().min(self.g_values.len());
128        for outer in 0..n {
129            for inner in 0..=outer {
130                if inner < self.g_values.len() && outer < self.f_values.len() {
131                    if self.g_values[inner] > self.f_values[outer] {
132                        return false;
133                    }
134                }
135            }
136        }
137        true
138    }
139    /// Returns the pointwise maximum of f and g (another majorant).
140    pub fn pointwise_max(&self) -> Vec<u64> {
141        let n = self.f_values.len().max(self.g_values.len());
142        (0..n)
143            .map(|i| {
144                let fv = self.f_values.get(i).copied().unwrap_or(0);
145                let gv = self.g_values.get(i).copied().unwrap_or(0);
146                fv.max(gv)
147            })
148            .collect()
149    }
150}
151/// Kleene's realizability / Kreisel's modified realizability.
152#[derive(Debug, Clone)]
153pub struct RealizabilityInterpretation {
154    /// Which variant: `"kleene"` or `"kreisel"`.
155    pub variant: String,
156    /// The formula being interpreted.
157    pub formula: RealizedFormula,
158    /// Whether the interpretation is constructive.
159    pub is_constructive: bool,
160}
161impl RealizabilityInterpretation {
162    /// Create a Kleene realizability interpretation.
163    pub fn kleene(formula: RealizedFormula) -> Self {
164        Self {
165            variant: "kleene".into(),
166            formula,
167            is_constructive: true,
168        }
169    }
170    /// Create a Kreisel modified-realizability interpretation.
171    pub fn kreisel(formula: RealizedFormula) -> Self {
172        Self {
173            variant: "kreisel".into(),
174            formula,
175            is_constructive: true,
176        }
177    }
178}
179#[allow(dead_code)]
180#[derive(Debug, Clone)]
181pub struct ProverData {
182    pub prover_name: String,
183    pub logic: String,
184    pub is_complete: bool,
185    pub is_sound: bool,
186    pub search_strategy: SearchStrategyNew,
187}
188#[allow(dead_code)]
189impl ProverData {
190    pub fn resolution_prover() -> Self {
191        ProverData {
192            prover_name: "Resolution Prover".to_string(),
193            logic: "Classical Propositional Logic".to_string(),
194            is_complete: true,
195            is_sound: true,
196            search_strategy: SearchStrategyNew::Saturation,
197        }
198    }
199    pub fn tableau_prover() -> Self {
200        ProverData {
201            prover_name: "Tableau Prover".to_string(),
202            logic: "Classical First-Order Logic".to_string(),
203            is_complete: true,
204            is_sound: true,
205            search_strategy: SearchStrategyNew::DepthFirst,
206        }
207    }
208    pub fn new_heuristic(name: &str, logic: &str, hint: &str) -> Self {
209        ProverData {
210            prover_name: name.to_string(),
211            logic: logic.to_string(),
212            is_complete: false,
213            is_sound: true,
214            search_strategy: SearchStrategyNew::Heuristic(hint.to_string()),
215        }
216    }
217    pub fn completeness_theorem(&self) -> String {
218        if self.is_complete {
219            format!(
220                "{}: complete for {} (every valid formula is provable)",
221                self.prover_name, self.logic
222            )
223        } else {
224            format!("{}: incomplete (heuristic only)", self.prover_name)
225        }
226    }
227    pub fn superposition_calculus_description(&self) -> String {
228        "Superposition: complete for equational logic, used in E, Vampire, SPASS".to_string()
229    }
230}
231/// A resolution refutation: derives ⊥ from a set of clauses.
232#[derive(Debug, Clone)]
233pub struct ResolutionRefutation {
234    /// The initial clause set.
235    pub clauses: Vec<Clause>,
236    /// The sequence of resolution steps.
237    pub steps: Vec<ResolutionStep>,
238}
239impl ResolutionRefutation {
240    /// Create a new refutation attempt from a clause set.
241    pub fn new(clauses: Vec<Clause>) -> Self {
242        Self {
243            clauses,
244            steps: Vec::new(),
245        }
246    }
247    /// Add a resolution step.
248    pub fn add_step(&mut self, step: ResolutionStep) {
249        self.steps.push(step);
250    }
251    /// Returns true if the last step produced the empty clause.
252    pub fn is_complete(&self) -> bool {
253        self.steps
254            .last()
255            .is_some_and(|s| s.resolvent.is_empty_clause())
256    }
257    /// Perform unit propagation: return the set of forced literals.
258    pub fn unit_propagate(&self) -> Vec<Literal> {
259        let mut forced: Vec<Literal> = Vec::new();
260        for clause in &self.clauses {
261            if clause.is_unit() {
262                if let Some(lit) = clause.literals.first() {
263                    if !forced.contains(lit) {
264                        forced.push(lit.clone());
265                    }
266                }
267            }
268        }
269        forced
270    }
271    /// A single DPLL-style split on the first unassigned variable.
272    pub fn dpll_step(&self) -> Option<u32> {
273        for clause in &self.clauses {
274            if let Some(lit) = clause.literals.first() {
275                return Some(lit.var);
276            }
277        }
278        None
279    }
280}
281/// Computable functional realizing ∀∃ statements under Dialectica.
282#[derive(Debug, Clone)]
283pub struct FunctionalInterpretation {
284    /// The formula being realized.
285    pub formula: DialecticaFormula,
286    /// Description of the realizing functional.
287    pub functional_description: String,
288}
289impl FunctionalInterpretation {
290    /// Create a new functional interpretation.
291    pub fn new(formula: DialecticaFormula, functional_description: impl Into<String>) -> Self {
292        Self {
293            formula,
294            functional_description: functional_description.into(),
295        }
296    }
297}
298/// Weak König's Lemma and its Dialectica interpretation.
299#[derive(Debug, Clone)]
300pub struct WeakKoenigsLemma {
301    /// WKL: every infinite binary tree has an infinite path.
302    pub statement: String,
303    /// Its Dialectica interpretation (skolemized).
304    pub dialectica_form: Option<DialecticaFormula>,
305}
306impl WeakKoenigsLemma {
307    /// Construct the standard WKL instance.
308    pub fn standard() -> Self {
309        Self {
310            statement: "Every infinite binary tree has an infinite path.".into(),
311            dialectica_form: None,
312        }
313    }
314    /// Return whether a Dialectica form has been computed.
315    pub fn has_dialectica_form(&self) -> bool {
316        self.dialectica_form.is_some()
317    }
318}
319/// Ramsey theory bounds from proof mining.
320#[allow(dead_code)]
321#[derive(Debug, Clone)]
322pub struct RamseyBound {
323    pub name: String,
324    pub lower_bound: u64,
325    pub upper_bound: Option<u64>,
326    pub proof_system: String,
327}
328impl RamseyBound {
329    #[allow(dead_code)]
330    pub fn r33() -> Self {
331        Self {
332            name: "R(3,3)".to_string(),
333            lower_bound: 6,
334            upper_bound: Some(6),
335            proof_system: "Elementary combinatorics".to_string(),
336        }
337    }
338    #[allow(dead_code)]
339    pub fn r44() -> Self {
340        Self {
341            name: "R(4,4)".to_string(),
342            lower_bound: 18,
343            upper_bound: Some(18),
344            proof_system: "Computer search + proof".to_string(),
345        }
346    }
347    #[allow(dead_code)]
348    pub fn is_exact(&self) -> bool {
349        self.upper_bound
350            .map(|u| u == self.lower_bound)
351            .unwrap_or(false)
352    }
353}
354/// Finitization of an infinite principle.
355#[allow(dead_code)]
356#[derive(Debug, Clone)]
357pub struct Finitization {
358    pub infinite_principle: String,
359    pub finite_version: String,
360    pub quantitative_bound: String,
361}
362impl Finitization {
363    #[allow(dead_code)]
364    pub fn new(inf: &str, fin: &str, bound: &str) -> Self {
365        Self {
366            infinite_principle: inf.to_string(),
367            finite_version: fin.to_string(),
368            quantitative_bound: bound.to_string(),
369        }
370    }
371    #[allow(dead_code)]
372    pub fn bolzano_weierstrass() -> Self {
373        Self::new(
374            "Every bounded sequence has a convergent subsequence",
375            "For every eps, there exist indices i < j s.t. |x_i - x_j| < eps",
376            "Omega(eps, M) primitive recursive in eps and bound M",
377        )
378    }
379    #[allow(dead_code)]
380    pub fn description(&self) -> String {
381        format!(
382            "Finite: {}\nfrom: {}\nbound: {}",
383            self.finite_version, self.infinite_principle, self.quantitative_bound
384        )
385    }
386}
387/// A clause: a disjunction of literals.
388#[derive(Debug, Clone, PartialEq, Eq)]
389pub struct Clause {
390    /// The literals in the clause.
391    pub literals: Vec<Literal>,
392}
393impl Clause {
394    /// Create an empty clause (represents ⊥).
395    pub fn empty() -> Self {
396        Self {
397            literals: Vec::new(),
398        }
399    }
400    /// Create a clause from a list of literals.
401    pub fn new(literals: Vec<Literal>) -> Self {
402        Self { literals }
403    }
404    /// Returns true if this is the empty clause (contradiction).
405    pub fn is_empty_clause(&self) -> bool {
406        self.literals.is_empty()
407    }
408    /// Returns true if the clause is a tautology (contains x and ¬x).
409    pub fn is_tautology(&self) -> bool {
410        for lit in &self.literals {
411            if self.literals.contains(&lit.complement()) {
412                return true;
413            }
414        }
415        false
416    }
417    /// Returns true if the clause is a unit clause (exactly one literal).
418    pub fn is_unit(&self) -> bool {
419        self.literals.len() == 1
420    }
421}
422/// Uniform convexity modulus.
423#[allow(dead_code)]
424#[derive(Debug, Clone)]
425pub struct UniformConvexityModulus {
426    pub space_name: String,
427    pub modulus: String,
428}
429impl UniformConvexityModulus {
430    #[allow(dead_code)]
431    pub fn new(space: &str, modulus: &str) -> Self {
432        Self {
433            space_name: space.to_string(),
434            modulus: modulus.to_string(),
435        }
436    }
437    #[allow(dead_code)]
438    pub fn hilbert_space() -> Self {
439        Self::new("Hilbert space H", "delta(eps) = 1 - sqrt(1 - eps^2/4)")
440    }
441    #[allow(dead_code)]
442    pub fn l_p_space(p: f64) -> Self {
443        let formula = if p >= 2.0 {
444            format!("delta(eps) >= (eps/2)^p / (2 max(1, 2^(p-2)))")
445        } else {
446            format!("delta(eps) >= (eps/2)^2 / 8 (Clarkson for p={p})")
447        };
448        Self::new(&format!("L^{p}"), &formula)
449    }
450    #[allow(dead_code)]
451    pub fn bound_on_iterations_for_mann(&self, _epsilon: f64) -> String {
452        format!(
453            "Kohlenbach-Leustean: rate of Mann iterations in {} via {}",
454            self.space_name, self.modulus
455        )
456    }
457}
458#[allow(dead_code)]
459#[derive(Debug, Clone)]
460pub enum SearchStrategyNew {
461    BreadthFirst,
462    DepthFirst,
463    IterativeDeepening,
464    Heuristic(String),
465    Saturation,
466}
467#[allow(dead_code)]
468impl SearchStrategyNew {
469    fn saturation_strategy() -> SearchStrategyNew {
470        SearchStrategyNew::Saturation
471    }
472}
473/// Termination argument via ordinals.
474#[allow(dead_code)]
475#[derive(Debug, Clone)]
476pub struct OrdinalTermination {
477    pub algorithm_name: String,
478    pub ordinal_bound: String,
479    pub is_primitive_recursive: bool,
480}
481impl OrdinalTermination {
482    #[allow(dead_code)]
483    pub fn new(alg: &str, bound: &str, prim_rec: bool) -> Self {
484        Self {
485            algorithm_name: alg.to_string(),
486            ordinal_bound: bound.to_string(),
487            is_primitive_recursive: prim_rec,
488        }
489    }
490    #[allow(dead_code)]
491    pub fn termination_proof(&self) -> String {
492        format!(
493            "{} terminates: assign ordinal {} decreasing at each step",
494            self.algorithm_name, self.ordinal_bound
495        )
496    }
497}
498/// Explicit witness extracted from a ∃x.P(x) proof (Herbrand's theorem).
499#[derive(Debug, Clone, PartialEq, Eq)]
500pub struct HerbrandTerm {
501    /// The variable bound by the quantifier.
502    pub variable: String,
503    /// The concrete term witnessing existence.
504    pub term: String,
505    /// The predicate P, as a string.
506    pub predicate: String,
507}
508impl HerbrandTerm {
509    /// Create a new Herbrand witness.
510    pub fn new(
511        variable: impl Into<String>,
512        term: impl Into<String>,
513        predicate: impl Into<String>,
514    ) -> Self {
515        Self {
516            variable: variable.into(),
517            term: term.into(),
518            predicate: predicate.into(),
519        }
520    }
521    /// Return a human-readable description of the witness.
522    pub fn describe(&self) -> String {
523        format!(
524            "∃ {}, {} [witness: {}]",
525            self.variable, self.predicate, self.term
526        )
527    }
528}
529/// A heuristic function: estimates the distance from a proof state to a complete proof.
530#[derive(Debug, Clone)]
531pub struct HeuristicFn {
532    /// Human-readable name of the heuristic.
533    pub name: String,
534}
535impl HeuristicFn {
536    /// Create a named heuristic.
537    pub fn new(name: impl Into<String>) -> Self {
538        Self { name: name.into() }
539    }
540    /// Estimate: simply return the number of remaining goals.
541    pub fn estimate(&self, state: &ProofState) -> usize {
542        state.goals.len()
543    }
544}
545/// A simple representation of ordinals below ε_0 in Cantor Normal Form.
546///
547/// An ordinal is represented as a sorted (descending) list of exponents,
548/// where the ordinal = ω^e₁ + ω^e₂ + … for e₁ ≥ e₂ ≥ …
549#[derive(Debug, Clone, PartialEq, Eq)]
550pub struct CantorNormalForm {
551    /// Exponents in descending order (each is a Cantor normal form itself,
552    /// but we represent exponents as u32 for finite ordinals below ε_0).
553    pub exponents: Vec<u32>,
554}
555impl CantorNormalForm {
556    /// The zero ordinal.
557    pub fn zero() -> Self {
558        Self { exponents: vec![] }
559    }
560    /// The ordinal 1 (= ω^0).
561    pub fn one() -> Self {
562        Self { exponents: vec![0] }
563    }
564    /// The ordinal ω (= ω^1).
565    pub fn omega() -> Self {
566        Self { exponents: vec![1] }
567    }
568    /// The ordinal ε_0 is represented as "the limit" — we use a sentinel.
569    pub fn epsilon0() -> Self {
570        Self {
571            exponents: vec![u32::MAX],
572        }
573    }
574    /// Returns true if this is the zero ordinal.
575    pub fn is_zero(&self) -> bool {
576        self.exponents.is_empty()
577    }
578    /// Compare two ordinals (both must be in CNF with u32 exponents).
579    pub fn less_than(&self, other: &Self) -> bool {
580        for (a, b) in self.exponents.iter().zip(other.exponents.iter()) {
581            if a < b {
582                return true;
583            }
584            if a > b {
585                return false;
586            }
587        }
588        self.exponents.len() < other.exponents.len()
589    }
590    /// Ordinal addition α + β in CNF.
591    pub fn add(&self, other: &Self) -> Self {
592        if other.is_zero() {
593            return self.clone();
594        }
595        let lead_b = other.exponents[0];
596        let mut result: Vec<u32> = self
597            .exponents
598            .iter()
599            .copied()
600            .filter(|&e| e > lead_b)
601            .collect();
602        result.extend_from_slice(&other.exponents);
603        Self { exponents: result }
604    }
605}
606/// Extracts computational content from a proof (Kohlenbach's proof mining).
607#[derive(Debug, Clone)]
608pub struct WitnessExtractor {
609    /// Human-readable description of the proof being mined.
610    pub proof_name: String,
611    /// The extracted witness terms (as strings for display).
612    pub witnesses: Vec<String>,
613    /// Upper bound on the number of computation steps.
614    pub bound: Option<u64>,
615}
616impl WitnessExtractor {
617    /// Create a new `WitnessExtractor` for the named proof.
618    pub fn new(proof_name: impl Into<String>) -> Self {
619        Self {
620            proof_name: proof_name.into(),
621            witnesses: Vec::new(),
622            bound: None,
623        }
624    }
625    /// Add an extracted witness term.
626    pub fn add_witness(&mut self, term: impl Into<String>) {
627        self.witnesses.push(term.into());
628    }
629    /// Return the first extracted witness, if any.
630    pub fn extract_witness(&self) -> Option<&str> {
631        self.witnesses.first().map(String::as_str)
632    }
633    /// Return the computed bound, or `u64::MAX` as a sentinel for "unknown".
634    pub fn compute_bound(&self) -> u64 {
635        self.bound.unwrap_or(u64::MAX)
636    }
637    /// Check whether at least one witness has been extracted.
638    pub fn is_realizable(&self) -> bool {
639        !self.witnesses.is_empty()
640    }
641}
642/// Current state of a proof search.
643#[derive(Debug, Clone)]
644pub struct ProofState {
645    /// Remaining goals as formula strings.
646    pub goals: Vec<String>,
647    /// Tactics applied so far.
648    pub applied_tactics: Vec<String>,
649    /// Remaining computational budget (steps).
650    pub budget: usize,
651}
652impl ProofState {
653    /// Create a proof state with a single goal and a budget.
654    pub fn new(goal: impl Into<String>, budget: usize) -> Self {
655        Self {
656            goals: vec![goal.into()],
657            applied_tactics: Vec::new(),
658            budget,
659        }
660    }
661    /// Returns true if all goals have been discharged.
662    pub fn is_complete(&self) -> bool {
663        self.goals.is_empty()
664    }
665    /// Apply a tactic name: removes the first goal and decrements budget.
666    pub fn apply_tactic(&mut self, tactic: impl Into<String>) -> bool {
667        if self.budget == 0 || self.goals.is_empty() {
668            return false;
669        }
670        self.goals.remove(0);
671        self.applied_tactics.push(tactic.into());
672        self.budget -= 1;
673        true
674    }
675}
676/// Proof complexity measure: size, depth, width, degree.
677#[derive(Debug, Clone, PartialEq, Eq)]
678pub struct ProofComplexityMeasure {
679    /// Total number of lines / nodes in the proof.
680    pub size: usize,
681    /// Maximum nesting depth.
682    pub depth: usize,
683    /// Maximum clause width (number of literals per clause).
684    pub width: usize,
685    /// Algebraic degree (for algebraic systems).
686    pub degree: usize,
687}
688impl ProofComplexityMeasure {
689    /// Construct a measure with all fields set to zero.
690    pub fn zero() -> Self {
691        Self {
692            size: 0,
693            depth: 0,
694            width: 0,
695            degree: 0,
696        }
697    }
698    /// Returns true if all measures are within the given bound.
699    pub fn is_within_bound(&self, bound: usize) -> bool {
700        self.size <= bound && self.depth <= bound && self.width <= bound && self.degree <= bound
701    }
702}
703/// The Cook-Reckhow theorem: NP ≠ co-NP iff no proof system is "efficient".
704#[derive(Debug, Clone)]
705pub struct CookReckhowThm {
706    /// Statement of the theorem.
707    pub statement: String,
708}
709impl CookReckhowThm {
710    /// Return the canonical statement of Cook-Reckhow.
711    pub fn canonical() -> Self {
712        Self {
713            statement: concat!(
714                "NP ≠ co-NP if and only if no propositional proof system ",
715                "polynomially simulates all others."
716            )
717            .into(),
718        }
719    }
720}
721/// Proof search strategy.
722#[derive(Debug, Clone, PartialEq, Eq)]
723pub enum SearchStrategy {
724    /// Depth-first search.
725    DFS,
726    /// Breadth-first search.
727    BFS,
728    /// A* (best-first with a heuristic).
729    AStar,
730    /// Iterative deepening depth-first search.
731    IDDFS,
732    /// Monte Carlo Tree Search.
733    MCTS,
734}
735/// Bounded model checking state: BMC encoding with a depth bound.
736#[derive(Debug, Clone)]
737pub struct ModelCheckingBound {
738    /// Current unfolding depth.
739    pub depth: usize,
740    /// Maximum depth allowed.
741    pub max_depth: usize,
742    /// Whether a counterexample was found within `depth` steps.
743    pub counterexample_found: bool,
744}
745impl ModelCheckingBound {
746    /// Create a bounded model checking instance.
747    pub fn new(max_depth: usize) -> Self {
748        Self {
749            depth: 0,
750            max_depth,
751            counterexample_found: false,
752        }
753    }
754    /// Increment the unfolding depth by one.
755    pub fn unfold(&mut self) {
756        if self.depth < self.max_depth {
757            self.depth += 1;
758        }
759    }
760    /// Returns true if the bound has been reached.
761    pub fn at_bound(&self) -> bool {
762        self.depth >= self.max_depth
763    }
764}
765/// An ML-like program extracted from a constructive proof.
766#[derive(Debug, Clone)]
767pub struct ExtractedProgram {
768    /// The source proposition / theorem.
769    pub source_theorem: String,
770    /// The program text (pseudo-ML).
771    pub program_text: String,
772    /// Whether the extraction is complete.
773    pub is_complete: bool,
774}
775impl ExtractedProgram {
776    /// Create a new extracted program.
777    pub fn new(theorem: impl Into<String>, program_text: impl Into<String>) -> Self {
778        Self {
779            source_theorem: theorem.into(),
780            program_text: program_text.into(),
781            is_complete: true,
782        }
783    }
784}
785/// Encodes Kohlenbach's monotone functional interpretation.
786#[derive(Debug, Clone)]
787pub struct MonotoneFunctionalInterpretation {
788    /// The formula being interpreted.
789    pub formula: String,
790    /// The majorizing functional (as a description string).
791    pub majorant: String,
792    /// Whether this is a bounded (monotone) interpretation.
793    pub is_bounded: bool,
794}
795impl MonotoneFunctionalInterpretation {
796    /// Create a new monotone functional interpretation.
797    pub fn new(formula: impl Into<String>, majorant: impl Into<String>) -> Self {
798        Self {
799            formula: formula.into(),
800            majorant: majorant.into(),
801            is_bounded: true,
802        }
803    }
804    /// Check whether the interpretation preserves the monotone bound.
805    pub fn check_bound(&self) -> bool {
806        !self.majorant.is_empty()
807    }
808}
809/// A propositional proof: a sequence of lines each with a justification.
810#[derive(Debug, Clone)]
811pub struct PropositionalProof {
812    /// The proof system used.
813    pub system: ProofSystem,
814    /// Lines: (formula_string, justification_string).
815    pub lines: Vec<(String, String)>,
816    /// The conclusion formula.
817    pub conclusion: String,
818}
819impl PropositionalProof {
820    /// Create an empty proof in the given system for the given conclusion.
821    pub fn new(system: ProofSystem, conclusion: impl Into<String>) -> Self {
822        Self {
823            system,
824            lines: Vec::new(),
825            conclusion: conclusion.into(),
826        }
827    }
828    /// Add a proof line with a justification.
829    pub fn add_line(&mut self, formula: impl Into<String>, justification: impl Into<String>) {
830        self.lines.push((formula.into(), justification.into()));
831    }
832    /// Return the proof complexity measure.
833    pub fn measure(&self) -> ProofComplexityMeasure {
834        ProofComplexityMeasure {
835            size: self.lines.len(),
836            depth: self.lines.len(),
837            width: self.lines.iter().map(|(f, _)| f.len()).max().unwrap_or(0),
838            degree: 0,
839        }
840    }
841}
842/// Well-founded induction certificate proving termination.
843#[derive(Debug, Clone)]
844pub struct TerminationProof {
845    /// The function name.
846    pub function_name: String,
847    /// The well-founded ordering used.
848    pub ordering: String,
849    /// Whether the termination argument has been fully verified.
850    pub verified: bool,
851}
852impl TerminationProof {
853    /// Create a termination proof by a given ordering.
854    pub fn new(function_name: impl Into<String>, ordering: impl Into<String>) -> Self {
855        Self {
856            function_name: function_name.into(),
857            ordering: ordering.into(),
858            verified: false,
859        }
860    }
861    /// Mark the termination proof as verified.
862    pub fn verify(&mut self) {
863        self.verified = true;
864    }
865}
866/// Proof mining in metric fixed point theory.
867#[allow(dead_code)]
868#[derive(Debug, Clone)]
869pub struct MetricFixedPointMining {
870    pub contraction_modulus: f64,
871    pub initial_error: f64,
872}
873impl MetricFixedPointMining {
874    #[allow(dead_code)]
875    pub fn new(q: f64, err: f64) -> Self {
876        assert!(q < 1.0, "Contraction constant must be < 1");
877        Self {
878            contraction_modulus: q,
879            initial_error: err,
880        }
881    }
882    #[allow(dead_code)]
883    pub fn iterations_to_epsilon(&self, epsilon: f64) -> u64 {
884        let n = (epsilon / self.initial_error).ln() / self.contraction_modulus.ln();
885        n.ceil() as u64
886    }
887    #[allow(dead_code)]
888    pub fn rate_of_convergence_description(&self) -> String {
889        format!(
890            "Banach iteration converges geometrically with ratio q = {}",
891            self.contraction_modulus
892        )
893    }
894}
895/// A literal: positive or negative occurrence of a variable.
896#[derive(Debug, Clone, PartialEq, Eq, Hash)]
897pub struct Literal {
898    /// The propositional variable index (1-based, SAT convention).
899    pub var: u32,
900    /// True for positive, false for negative.
901    pub positive: bool,
902}
903impl Literal {
904    /// Create a positive literal for variable `var`.
905    pub fn pos(var: u32) -> Self {
906        Self {
907            var,
908            positive: true,
909        }
910    }
911    /// Create a negative literal for variable `var`.
912    pub fn neg(var: u32) -> Self {
913        Self {
914            var,
915            positive: false,
916        }
917    }
918    /// Return the complementary literal.
919    pub fn complement(&self) -> Self {
920        Self {
921            var: self.var,
922            positive: !self.positive,
923        }
924    }
925}
926/// A formula together with its realizability status.
927#[derive(Debug, Clone, PartialEq, Eq)]
928pub enum RealizedFormula {
929    /// An atomic proposition identified by name.
930    Atomic(String),
931    /// Conjunction A ∧ B, realized by a pair of realizers.
932    Conjunction(Box<RealizedFormula>, Box<RealizedFormula>),
933    /// Disjunction A ∨ B, realized by a tagged realizer.
934    Disjunction(Box<RealizedFormula>, Box<RealizedFormula>),
935    /// Implication A → B, realized by a computable function.
936    Implication(Box<RealizedFormula>, Box<RealizedFormula>),
937    /// Universal quantification ∀x.A(x), realized for each input.
938    Forall(String, Box<RealizedFormula>),
939    /// Existential quantification ∃x.A(x), realized by a witness + proof.
940    Exists(String, Box<RealizedFormula>),
941}
942impl RealizedFormula {
943    /// Returns the depth of the formula tree.
944    pub fn depth(&self) -> usize {
945        match self {
946            RealizedFormula::Atomic(_) => 0,
947            RealizedFormula::Forall(_, f) | RealizedFormula::Exists(_, f) => 1 + f.depth(),
948            RealizedFormula::Conjunction(a, b)
949            | RealizedFormula::Disjunction(a, b)
950            | RealizedFormula::Implication(a, b) => 1 + a.depth().max(b.depth()),
951        }
952    }
953    /// Returns true if the formula is existential at the top level.
954    pub fn is_existential(&self) -> bool {
955        matches!(self, RealizedFormula::Exists(_, _))
956    }
957}
958/// Systematic proof searcher with backtracking.
959#[derive(Debug, Clone)]
960pub struct ProofSearcher {
961    /// The search strategy.
962    pub strategy: SearchStrategy,
963    /// The heuristic function (used by A* and MCTS).
964    pub heuristic: HeuristicFn,
965    /// Maximum search depth.
966    pub max_depth: usize,
967}
968impl ProofSearcher {
969    /// Create a new proof searcher.
970    pub fn new(strategy: SearchStrategy, max_depth: usize) -> Self {
971        Self {
972            strategy,
973            heuristic: HeuristicFn::new("goal_count"),
974            max_depth,
975        }
976    }
977    /// Attempt to search for a proof of `goal` using `tactics`.
978    /// Returns the proof state if a complete proof is found.
979    pub fn search(&self, goal: impl Into<String>, tactics: &[&str]) -> Option<ProofState> {
980        let mut state = ProofState::new(goal, self.max_depth);
981        for tactic in tactics {
982            if state.is_complete() {
983                break;
984            }
985            state.apply_tactic(*tactic);
986        }
987        if state.is_complete() {
988            Some(state)
989        } else {
990            None
991        }
992    }
993}
994/// Encodes Tao's metastability bound Φ(ε, k) for a convergent sequence.
995///
996/// A sequence (a_n) is metastable with rate Φ if for every ε > 0 and k,
997/// there exists n ≤ Φ(ε, k) such that |a_n - a_{n+1}| < ε for all
998/// indices in [n, n + k].
999#[derive(Debug, Clone)]
1000pub struct MetastabilityBound {
1001    /// Name of the theorem/sequence this bound applies to.
1002    pub name: String,
1003    /// The bound function Φ: (epsilon_inv, steps) → index bound.
1004    /// We represent ε as its inverse (a natural number).
1005    pub bound_table: Vec<Vec<u64>>,
1006    /// Whether the bound is tight (matches known lower bounds).
1007    pub is_tight: bool,
1008}
1009impl MetastabilityBound {
1010    /// Create a metastability bound with a constant Φ(ε_inv, k) = c.
1011    pub fn constant(name: impl Into<String>, c: u64) -> Self {
1012        let table: Vec<Vec<u64>> = (0..8).map(|_| (0..8).map(|_| c).collect()).collect();
1013        Self {
1014            name: name.into(),
1015            bound_table: table,
1016            is_tight: false,
1017        }
1018    }
1019    /// Evaluate Φ(epsilon_inv, k): look up the bound table, clamped.
1020    pub fn evaluate(&self, epsilon_inv: usize, k: usize) -> u64 {
1021        let r = epsilon_inv.min(self.bound_table.len() - 1);
1022        let c = k.min(self.bound_table[r].len() - 1);
1023        self.bound_table[r][c]
1024    }
1025    /// Returns true if the bound is finite for all inputs.
1026    pub fn is_finite(&self) -> bool {
1027        self.bound_table
1028            .iter()
1029            .all(|row| row.iter().all(|&v| v < u64::MAX))
1030    }
1031}
1032/// A single resolution step: C_1 ∨ x, C_2 ∨ ¬x ⊢ C_1 ∨ C_2.
1033#[derive(Debug, Clone)]
1034pub struct ResolutionStep {
1035    /// First parent clause (contains `pivot` positively).
1036    pub parent1: Clause,
1037    /// Second parent clause (contains `pivot` negatively).
1038    pub parent2: Clause,
1039    /// The pivot variable.
1040    pub pivot: u32,
1041    /// The resolvent clause.
1042    pub resolvent: Clause,
1043}
1044impl ResolutionStep {
1045    /// Attempt to resolve `c1` and `c2` on variable `pivot`.
1046    /// Returns `None` if the pivot does not appear with opposite signs.
1047    pub fn resolve(c1: &Clause, c2: &Clause, pivot: u32) -> Option<Self> {
1048        let has_pos = c1.literals.iter().any(|l| l.var == pivot && l.positive);
1049        let has_neg = c2.literals.iter().any(|l| l.var == pivot && !l.positive);
1050        if !has_pos || !has_neg {
1051            return None;
1052        }
1053        let mut res_lits: Vec<Literal> = c1
1054            .literals
1055            .iter()
1056            .filter(|l| l.var != pivot)
1057            .chain(c2.literals.iter().filter(|l| l.var != pivot))
1058            .cloned()
1059            .collect();
1060        res_lits.sort_by_key(|l| (l.var, l.positive));
1061        res_lits.dedup();
1062        Some(ResolutionStep {
1063            parent1: c1.clone(),
1064            parent2: c2.clone(),
1065            pivot,
1066            resolvent: Clause::new(res_lits),
1067        })
1068    }
1069}
1070/// Spector bar recursion.
1071#[allow(dead_code)]
1072#[derive(Debug, Clone)]
1073pub struct BarRecursion {
1074    pub type_level: usize,
1075    pub models_comprehension: bool,
1076}
1077impl BarRecursion {
1078    #[allow(dead_code)]
1079    pub fn spector() -> Self {
1080        Self {
1081            type_level: 2,
1082            models_comprehension: true,
1083        }
1084    }
1085    #[allow(dead_code)]
1086    pub fn description(&self) -> String {
1087        format!(
1088            "Spector bar recursion: models classical comprehension via type-{} functional",
1089            self.type_level
1090        )
1091    }
1092    #[allow(dead_code)]
1093    pub fn kohlenbach_generalization(&self) -> String {
1094        "Modified bar recursion for non-empty types (Berger-Oliva)".to_string()
1095    }
1096}
1097/// Quantitative Cauchy sequence criterion.
1098#[allow(dead_code)]
1099#[derive(Debug, Clone)]
1100pub struct QuantitativeCauchy {
1101    pub space_name: String,
1102    pub convergence_rate: String,
1103}
1104impl QuantitativeCauchy {
1105    #[allow(dead_code)]
1106    pub fn new(space: &str, rate: &str) -> Self {
1107        Self {
1108            space_name: space.to_string(),
1109            convergence_rate: rate.to_string(),
1110        }
1111    }
1112    #[allow(dead_code)]
1113    pub fn leustean_bound_for_cat0(&self) -> String {
1114        "Leustean: Halpern iterations converge in CAT(0) spaces with explicit rate omega^omega"
1115            .to_string()
1116    }
1117}
1118/// Gödel's Dialectica translation A^D as (∃u.∀x. A_D(u,x)).
1119#[derive(Debug, Clone)]
1120pub struct DialecticaFormula {
1121    /// The original formula A.
1122    pub original: String,
1123    /// The universal variable names (the "x" side).
1124    pub universal_vars: Vec<String>,
1125    /// The existential variable names (the "u" side).
1126    pub existential_vars: Vec<String>,
1127    /// The quantifier-free body A_D(u,x), as a string.
1128    pub body: String,
1129}
1130impl DialecticaFormula {
1131    /// Create the Dialectica translation of a formula.
1132    pub fn translate(original: impl Into<String>, body: impl Into<String>) -> Self {
1133        Self {
1134            original: original.into(),
1135            universal_vars: vec!["x".into()],
1136            existential_vars: vec!["u".into()],
1137            body: body.into(),
1138        }
1139    }
1140    /// Return the full translated formula as a string.
1141    pub fn display(&self) -> String {
1142        format!(
1143            "∃ {}. ∀ {}. {}",
1144            self.existential_vars.join(", "),
1145            self.universal_vars.join(", "),
1146            self.body,
1147        )
1148    }
1149}
1150/// A polynomial or exponential complexity bound extracted from a proof.
1151#[derive(Debug, Clone, PartialEq, Eq)]
1152pub enum ComplexityBound {
1153    /// Constant O(1).
1154    Constant,
1155    /// Linear O(n).
1156    Linear,
1157    /// Polynomial O(n^k) for given k.
1158    Polynomial(u32),
1159    /// Exponential O(2^n).
1160    Exponential,
1161    /// Non-elementary.
1162    NonElementary,
1163}
1164impl ComplexityBound {
1165    /// Returns true if the bound is at most polynomial.
1166    pub fn is_polynomial(&self) -> bool {
1167        matches!(
1168            self,
1169            ComplexityBound::Constant | ComplexityBound::Linear | ComplexityBound::Polynomial(_)
1170        )
1171    }
1172}
1173/// Builds Herbrand sequences from a first-order formula.
1174#[derive(Debug, Clone)]
1175pub struct HerbrandSequenceBuilder {
1176    /// The original formula (as a string).
1177    pub formula: String,
1178    /// The ground instances collected so far.
1179    pub instances: Vec<String>,
1180    /// Maximum number of instances to generate.
1181    pub max_instances: usize,
1182}
1183impl HerbrandSequenceBuilder {
1184    /// Create a new builder for the given formula.
1185    pub fn new(formula: impl Into<String>, max_instances: usize) -> Self {
1186        Self {
1187            formula: formula.into(),
1188            instances: Vec::new(),
1189            max_instances,
1190        }
1191    }
1192    /// Add a ground instance (substituting concrete terms for free variables).
1193    pub fn add_instance(&mut self, instance: impl Into<String>) -> bool {
1194        if self.instances.len() >= self.max_instances {
1195            return false;
1196        }
1197        self.instances.push(instance.into());
1198        true
1199    }
1200    /// Return true if the disjunction of all instances is a tautology (checked syntactically).
1201    pub fn is_tautology(&self) -> bool {
1202        self.instances.iter().any(|s| s.contains("True"))
1203    }
1204    /// Return the Herbrand complexity (number of instances).
1205    pub fn complexity(&self) -> usize {
1206        self.instances.len()
1207    }
1208    /// Return the disjunction of all collected instances.
1209    pub fn disjunction(&self) -> String {
1210        if self.instances.is_empty() {
1211            return "False".to_string();
1212        }
1213        self.instances.join(" ∨ ")
1214    }
1215}
1216#[allow(dead_code)]
1217#[derive(Debug, Clone)]
1218pub struct GentzenNormalization {
1219    pub proof_size_before: usize,
1220    pub proof_size_after: usize,
1221    pub cut_rank: usize,
1222    pub num_reduction_steps: usize,
1223}
1224#[allow(dead_code)]
1225impl GentzenNormalization {
1226    pub fn new(before: usize, cut_rank: usize) -> Self {
1227        let steps = 2_usize.saturating_pow(cut_rank as u32);
1228        GentzenNormalization {
1229            proof_size_before: before,
1230            proof_size_after: before * steps,
1231            cut_rank,
1232            num_reduction_steps: steps,
1233        }
1234    }
1235    pub fn cut_elimination_theorem(&self) -> String {
1236        format!(
1237            "Gentzen's cut elimination: proof of size {} with cut rank {} → normal proof of size {} (TOWER({}))",
1238            self.proof_size_before, self.cut_rank, self.proof_size_after, self.cut_rank
1239        )
1240    }
1241    pub fn reduction_terminates(&self) -> bool {
1242        true
1243    }
1244    pub fn ordinal_analysis_connection(&self) -> String {
1245        "PA cut-rank ↔ ordinal ε₀; PA₂ ↔ Γ₀; KP ↔ Bachmann-Howard ordinal".to_string()
1246    }
1247}
1248#[allow(dead_code)]
1249#[derive(Debug, Clone)]
1250pub enum ProofSystemType {
1251    Resolution,
1252    Frege,
1253    ExtendedFrege,
1254    QuantifiedPropositional,
1255    CuttingPlanes,
1256    SumOfSquares,
1257}
1258#[allow(dead_code)]
1259#[derive(Debug, Clone)]
1260pub struct PhpPrinciple {
1261    pub n_pigeons: usize,
1262    pub m_holes: usize,
1263    pub resolution_lower_bound: usize,
1264}
1265#[allow(dead_code)]
1266impl PhpPrinciple {
1267    pub fn new(n: usize, m: usize) -> Self {
1268        let lb = 2_usize.saturating_pow((n / 2) as u32);
1269        PhpPrinciple {
1270            n_pigeons: n,
1271            m_holes: m,
1272            resolution_lower_bound: lb,
1273        }
1274    }
1275    pub fn is_valid_php(&self) -> bool {
1276        self.n_pigeons > self.m_holes
1277    }
1278    pub fn haken_lower_bound_description(&self) -> String {
1279        format!(
1280            "Haken (1985): PHP_{} has no polynomial resolution proof; lower bound ≥ {}",
1281            self.n_pigeons, self.resolution_lower_bound
1282        )
1283    }
1284    pub fn bounded_arithmetic_connection(&self) -> String {
1285        format!(
1286            "PHP_{} unprovable in S^1_2 but provable in T^2_2 (bounded arithmetic)",
1287            self.n_pigeons
1288        )
1289    }
1290}
1291/// A propositional proof system.
1292#[derive(Debug, Clone, PartialEq, Eq, Hash)]
1293pub enum ProofSystem {
1294    /// Resolution (Robinson 1965).
1295    Resolution,
1296    /// Frege / Hilbert-style propositional calculus.
1297    Frege,
1298    /// Extended Frege (with extension axioms).
1299    ExtendedFrege,
1300    /// Half-Frege (bounded-depth Frege).
1301    HalfFrege,
1302    /// Cutting Planes (LP relaxation cuts).
1303    CuttingPlanes,
1304    /// Nullstellensatz proof system (algebraic).
1305    Nullstellensatz,
1306    /// Sum-of-Squares (Positivstellensatz).
1307    SOS,
1308    /// Ideal Proof System (IPS).
1309    IPS,
1310}
1311/// A resolution proof: a DAG of resolution steps.
1312#[derive(Debug, Clone)]
1313pub struct ResolutionProof {
1314    /// The input clause set.
1315    pub input_clauses: Vec<Vec<i32>>,
1316    /// Resolution steps: (parent1_idx, parent2_idx, pivot_var, resolvent).
1317    pub steps: Vec<(usize, usize, i32, Vec<i32>)>,
1318}
1319impl ResolutionProof {
1320    /// Create a new resolution proof from the given input clauses.
1321    pub fn new(input_clauses: Vec<Vec<i32>>) -> Self {
1322        Self {
1323            input_clauses,
1324            steps: Vec::new(),
1325        }
1326    }
1327    /// Add a resolution step.
1328    pub fn add_step(&mut self, p1: usize, p2: usize, pivot: i32, resolvent: Vec<i32>) {
1329        self.steps.push((p1, p2, pivot, resolvent));
1330    }
1331    /// Returns true if the proof ends with the empty clause.
1332    pub fn is_refutation(&self) -> bool {
1333        self.steps.last().is_some_and(|(_, _, _, r)| r.is_empty())
1334    }
1335}
1336/// Effective bound extraction result.
1337#[allow(dead_code)]
1338#[derive(Debug, Clone)]
1339pub struct EffectiveBound {
1340    pub original_theorem: String,
1341    pub extracted_bound: String,
1342    pub bound_type: BoundType,
1343    pub dependencies: Vec<String>,
1344}
1345impl EffectiveBound {
1346    #[allow(dead_code)]
1347    pub fn new(theorem: &str, bound: &str, bt: BoundType) -> Self {
1348        Self {
1349            original_theorem: theorem.to_string(),
1350            extracted_bound: bound.to_string(),
1351            bound_type: bt,
1352            dependencies: Vec::new(),
1353        }
1354    }
1355    #[allow(dead_code)]
1356    pub fn is_feasible(&self) -> bool {
1357        matches!(self.bound_type, BoundType::Polynomial)
1358    }
1359    #[allow(dead_code)]
1360    pub fn add_dependency(&mut self, dep: &str) {
1361        self.dependencies.push(dep.to_string());
1362    }
1363}
1364/// Unwinding theorem: proof mining extracts computational content.
1365#[allow(dead_code)]
1366#[derive(Debug, Clone)]
1367pub struct UnwindingResult {
1368    pub classical_proof: String,
1369    pub constructive_content: String,
1370    pub interpreter_used: String,
1371}
1372impl UnwindingResult {
1373    #[allow(dead_code)]
1374    pub fn new(classical: &str, constructive: &str, interp: &str) -> Self {
1375        Self {
1376            classical_proof: classical.to_string(),
1377            constructive_content: constructive.to_string(),
1378            interpreter_used: interp.to_string(),
1379        }
1380    }
1381    #[allow(dead_code)]
1382    pub fn kohlenbach_style(&self) -> String {
1383        format!(
1384            "Kohlenbach unwinding: {} -> {}, via {}",
1385            self.classical_proof, self.constructive_content, self.interpreter_used
1386        )
1387    }
1388}
1389#[allow(dead_code)]
1390#[derive(Debug, Clone)]
1391pub struct ProofSystemNew {
1392    pub name: String,
1393    pub system_type: ProofSystemType,
1394    pub propositional_completeness: bool,
1395    pub p_simulates_resolution: Option<bool>,
1396}
1397#[allow(dead_code)]
1398impl ProofSystemNew {
1399    pub fn resolution() -> Self {
1400        ProofSystemNew {
1401            name: "Resolution".to_string(),
1402            system_type: ProofSystemType::Resolution,
1403            propositional_completeness: true,
1404            p_simulates_resolution: Some(false),
1405        }
1406    }
1407    pub fn frege() -> Self {
1408        ProofSystemNew {
1409            name: "Frege (Hilbert-style)".to_string(),
1410            system_type: ProofSystemType::Frege,
1411            propositional_completeness: true,
1412            p_simulates_resolution: Some(true),
1413        }
1414    }
1415    pub fn extended_frege() -> Self {
1416        ProofSystemNew {
1417            name: "Extended Frege (EF)".to_string(),
1418            system_type: ProofSystemType::ExtendedFrege,
1419            propositional_completeness: true,
1420            p_simulates_resolution: Some(true),
1421        }
1422    }
1423    pub fn separating_tautologies(&self) -> String {
1424        match &self.system_type {
1425            ProofSystemType::Resolution => {
1426                "Pigeonhole principle requires exponential-size Resolution proofs".to_string()
1427            }
1428            ProofSystemType::CuttingPlanes => {
1429                "CP: exponential lower bounds for random CNF (Razborov)".to_string()
1430            }
1431            _ => "Known lower bounds: PHP, Tseitin, Random k-CNF".to_string(),
1432        }
1433    }
1434    pub fn cook_reckhow_theorem(&self) -> String {
1435        "Cook-Reckhow: P=NP iff every Cook system has polynomial-size proofs".to_string()
1436    }
1437}
1438/// PA^ω conservativity results for bounded arithmetic.
1439#[derive(Debug, Clone)]
1440pub struct BoundedArithmetic {
1441    /// The theory name (e.g. "PA^ω", "WKL_0").
1442    pub theory: String,
1443    /// The base theory it is conservative over (e.g. "PRA").
1444    pub base_theory: String,
1445    /// Formula class for which conservativity holds.
1446    pub formula_class: String,
1447}
1448impl BoundedArithmetic {
1449    /// PA^ω is Π^0_2-conservative over PRA.
1450    pub fn paomega_over_pra() -> Self {
1451        Self {
1452            theory: "PA^ω".into(),
1453            base_theory: "PRA".into(),
1454            formula_class: "Π^0_2".into(),
1455        }
1456    }
1457}
1458#[allow(dead_code)]
1459#[derive(Debug, Clone, PartialEq, Eq)]
1460pub enum BoundType {
1461    Polynomial,
1462    Exponential,
1463    PrimitiveRecursive,
1464    Ackermann,
1465    NonPrimitive,
1466}
oxilean_std/proof_mining/types.rs

oxilean_std/proof_mining/
types.rs
