Expand description
Auto-generated module
🤖 Generated with SplitRS
Structs§
- BarRecursion
- Spector bar recursion.
- Bounded
Arithmetic - PA^ω conservativity results for bounded arithmetic.
- Cantor
Normal Form - A simple representation of ordinals below ε_0 in Cantor Normal Form.
- Clause
- A clause: a disjunction of literals.
- Cook
Reckhow Thm - The Cook-Reckhow theorem: NP ≠ co-NP iff no proof system is “efficient”.
- Curry
Howard - Proof-as-program correspondence (Curry-Howard).
- Dialectica
Formula - Gödel’s Dialectica translation A^D as (∃u.∀x. A_D(u,x)).
- Dialectica
Interp - Effective
Bound - Effective bound extraction result.
- Empty
Clause - The empty clause ⊥ (proof of contradiction).
- Extracted
Program - An ML-like program extracted from a constructive proof.
- Finitization
- Finitization of an infinite principle.
- Functional
Interpretation - Computable functional realizing ∀∃ statements under Dialectica.
- Gentzen
Normalization - Godel
Interpretation - G_del functional interpretation.
- Herbrand
Sequence Builder - Builds Herbrand sequences from a first-order formula.
- Herbrand
Term - Explicit witness extracted from a ∃x.P(x) proof (Herbrand’s theorem).
- Heuristic
Fn - A heuristic function: estimates the distance from a proof state to a complete proof.
- Literal
- A literal: positive or negative occurrence of a variable.
- Majorizability
Checker - Checks Howard/Bezem majorizability for a pair of functions (represented as tables).
- Metastability
Bound - Encodes Tao’s metastability bound Φ(ε, k) for a convergent sequence.
- Metric
Fixed Point Mining - Proof mining in metric fixed point theory.
- Model
Checking Bound - Bounded model checking state: BMC encoding with a depth bound.
- Monotone
Functional Interpretation - Encodes Kohlenbach’s monotone functional interpretation.
- Ordinal
Termination - Termination argument via ordinals.
- PhpPrinciple
- Proof
Complexity Measure - Proof complexity measure: size, depth, width, degree.
- Proof
Searcher - Systematic proof searcher with backtracking.
- Proof
State - Current state of a proof search.
- Proof
System New - Propositional
Proof - A propositional proof: a sequence of lines each with a justification.
- Prover
Data - Quantitative
Cauchy - Quantitative Cauchy sequence criterion.
- Ramsey
Bound - Ramsey theory bounds from proof mining.
- Realizability
Interpretation - Kleene’s realizability / Kreisel’s modified realizability.
- Resolution
Proof - A resolution proof: a DAG of resolution steps.
- Resolution
Refutation - A resolution refutation: derives ⊥ from a set of clauses.
- Resolution
Step - A single resolution step: C_1 ∨ x, C_2 ∨ ¬x ⊢ C_1 ∨ C_2.
- Termination
Proof - Well-founded induction certificate proving termination.
- Uniform
Convexity Modulus - Uniform convexity modulus.
- Unwinding
Result - Unwinding theorem: proof mining extracts computational content.
- Weak
Koenigs Lemma - Weak König’s Lemma and its Dialectica interpretation.
- Witness
Extractor - Extracts computational content from a proof (Kohlenbach’s proof mining).
Enums§
- Bound
Type - Complexity
Bound - A polynomial or exponential complexity bound extracted from a proof.
- Proof
System - A propositional proof system.
- Proof
System Type - Realized
Formula - A formula together with its realizability status.
- Search
Strategy - Proof search strategy.
- Search
Strategy New