Certified equational reasoning via ordered completion
From MaRDI portal
Publication:2305436
DOI10.1007/978-3-030-29436-6_30OpenAlexW2969538927MaRDI QIDQ2305436
Sarah Winkler, Christian Sternagel
Publication date: 10 March 2020
Full work available at URL: https://doi.org/10.1007/978-3-030-29436-6_30
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- On ground-confluence of term rewriting systems
- Solution of the Robbins problem
- On using ground joinable equations in equational theorem proving
- Isabelle/HOL. A proof assistant for higher-order logic
- MædMax: a maximal ordered completion tool
- Short single axioms for Boolean algebra
- Certified equational reasoning via ordered completion
- A transfinite Knuth-Bendix order for lambda-free higher-order terms
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion
- Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion
- Code Generation via Higher-Order Rewrite Systems
- Signature Extensions Preserve Termination
- Algebraic data integration
- Term Rewriting and All That
- Conditional Confluence (System Description)
- Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion
This page was built for publication: Certified equational reasoning via ordered completion
