The following pages link to Theorem proving modulo (Q1431339):
Displaying 18 items.
- Proof generalization in \(\mathrm {LK}\) by second order unifier minimization (Q331619) (← 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)
- Theorem proving modulo (Q1431339) (← 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)
- (Q5089014) (← links)
- High-Level Theories (Q5505502) (← links)
- Analogy in Automated Deduction: A Survey (Q5739522) (← links)
- Extensional proofs in a propositional logic modulo isomorphisms (Q6052705) (← links)
