The following pages link to Theorem proving modulo (Q1431339):
Displaying 50 items.
- Proof generalization in \(\mathrm {LK}\) by second order unifier minimization (Q331619) (← links)
- A simple proof that super-consistency implies cut elimination (Q691121) (← links)
- PNL to HOL: from the logic of nominal sets to the logic of higher-order functions (Q714797) (← links)
- CERES in higher-order logic (Q716500) (← links)
- On the expressive power of schemes (Q719245) (← links)
- Clausal presentation of theories in deduction modulo (Q744331) (← links)
- Resolution is cut-free (Q972424) (← links)
- The proof monad (Q974136) (← links)
- On the confluence of lambda-calculus with conditional rewriting (Q987976) (← links)
- Inductive proof search modulo (Q1037404) (← links)
- Differential dynamic logic for hybrid systems (Q1040772) (← links)
- Lazy techniques for fully expansive theorem proving (Q1309245) (← links)
- Theorem proving modulo (Q1431339) (← links)
- ELAN from a rewriting logic point of view (Q1608914) (← links)
- Equational rules for rewriting logic (Q1608925) (← links)
- Rewriting logic: Roadmap and bibliography (Q1615001) (← links)
- Aligning concepts across proof assistant libraries (Q1640642) (← links)
- A semantic framework for proof evidence (Q1701039) (← links)
- A complete uniform substitution calculus for differential dynamic logic (Q1707599) (← links)
- Some general results about proof normalization (Q1931341) (← links)
- Twenty years of rewriting logic (Q1931904) (← links)
- Equational theorem proving modulo (Q2055853) (← links)
- A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems (Q2095424) (← links)
- From the universality of mathematical truth to the interoperability of proof systems (Q2104491) (← links)
- \textsf{Goéland}: a concurrent tableau-based theorem prover (system description) (Q2104525) (← links)
- First-order automated reasoning with theories: when deduction modulo theory meets practice (Q2209546) (← links)
- Physics and proof theory (Q2249005) (← links)
- Regaining cut admissibility in deduction modulo using abstract completion (Q2266989) (← links)
- Restricted combinatory unification (Q2305407) (← links)
- Automatically proving equivalence by type-safe reflection (Q2364699) (← links)
- Dealing with algebraic expressions over a field in Coq using Maple (Q2456560) (← links)
- Superposition with equivalence reasoning and delayed clause normal form transformation (Q2486577) (← links)
- Abstract canonical presentations (Q2500482) (← links)
- Eigenvariables, bracketing and the decidability of positive minimal predicate logic (Q2503325) (← links)
- Semantic foundations for generalized rewrite theories (Q2503334) (← links)
- Certifying term rewriting proofs in ELAN (Q2841249) (← links)
- A framework for defining logical frameworks (Q2864157) (← links)
- On the convergence of reduction-based and model-based methods in proof theory (Q2866742) (← links)
- Orthogonality and Boolean Algebras for Deduction Modulo (Q3007658) (← links)
- CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates (Q3094178) (← links)
- A Proposal for Broad Spectrum Proof Certificates (Q3100201) (← links)
- Soundly Proving B Method Formulæ Using Typed Sequent Calculus (Q3179401) (← links)
- Verificationism and Classical Realizability (Q3305313) (← links)
- CTL Model Checking in Deduction Modulo (Q3454102) (← links)
- Integrating Simplex with Tableaux (Q3455763) (← links)
- Strong normalisation in two Pure Pattern Type Systems (Q3520143) (← links)
- A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms (Q3540178) (← links)
- Axiom Directed Focusing (Q3638252) (← links)
- Automating Theories in Intuitionistic Logic (Q3655199) (← links)
- (Q4539633) (← links)
