scientific article; zbMATH DE number 7204430

DOI10.4230/LIPICS.FSCD.2017.11zbMATH Open1434.03025MaRDI QIDQ5111307FDOQ5111307

Dmitriy Traytel, Jasmin Christian Blanchette, Mathias Fleury

Publication date: 26 May 2020

Title of this publication is not available (Why is that?)

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)

Cites Work

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

Cited In (3)

• Type-theoretic approaches to ordinals
• Title not available (Why is that?)
• Formalizing Bachmair and Ganzinger's ordered resolution prover

Uses Software

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

Recommendations

• Title not available (Why is that?) 👍 👎
• Hierarchies of monadic generalized quantifiers 👍 👎
• Nested sequents for intuitionistic logics 👍 👎
• Isabelle Formalization of Set Theoretic Structures and Set Comprehensions 👍 👎
• Higher-Order Separation Logic in Isabelle/HOLCF 👍 👎
• Multisets in type theory 👍 👎
• Higher-Order Abstract Syntax in Isabelle/HOL 👍 👎
• Multitraces, hypertraces and partial order semantics 👍 👎
• Isabelle/HOL/GST: a formal proof environment for generalized set theories 👍 👎
• Hereditarily Finite Sets in Constructive Type Theory 👍 👎

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5111307)