scientific article; zbMATH DE number 7204430

DOI10.4230/LIPIcs.FSCD.2017.11zbMath1434.03025MaRDI QIDQ5111307

Dmitriy Traytel, Jasmin Christian Blanchette, Mathias Fleury

Publication date: 26 May 2020

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

proof assistantsmultisetsordinals

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Recursive ordinals and ordinal notations (03F15)

Related Items (3)

Type-theoretic approaches to ordinals ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover ⋮ Unnamed Item

Uses Software

• Isabelle/HOL
• Isar
• Sledgehammer
• HOCL
• CoLoR
• Transfer
• Lifting
• Knuth Bendix Orders
• Archive Formal Proofs
• Lambda Free RPOs
• Nested Multisets

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations
• LCF considered as a programming language
• Unary PCF is decidable
• Decidability of behavioural equivalence in unary PCF
• Isabelle/HOL. A proof assistant for higher-order logic
• A mechanizable first-order theory of ordinals
• A transfinite Knuth-Bendix order for lambda-free higher-order terms
• A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
• Truly Modular (Co)datatypes for Isabelle/HOL
• Cardinals in Isabelle/HOL
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
• A Lambda-Free Higher-Order Recursive Path Order
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates
• An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
• Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
• Building Formal Method Tools in the Isabelle/Isar Framework
• Certification of Automated Termination Proofs
• Certified Size-Change Termination
• The Hydra Battle Revisited
• Partial Recursive Functions in Higher-Order Logic
• Proving termination with multiset orderings
• Accessible Independence Results for Peano Arithmetic
• Setoids in type theory
• On the Formalization of Termination Techniques based on Multiset Orderings
• Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω 1
• Generalised multisets for chemical programming
• On the restricted ordinal theorem
• General Bindings and Alpha-Equivalence in Nominal Isabelle

This page was built for publication: