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?)

Recommendations

• Isabelle formalization of set theoretic structures and set comprehensions
• Hereditarily finite sets in constructive type theory
• Multisets in type theory
• Nested sequents for intuitionistic logics
• Higher-order abstract syntax in Isabelle/HOL
• Isabelle/HOL/GST: a formal proof environment for generalized set theories
• Multitraces, hypertraces and partial order semantics
• Hierarchies of monadic generalized quantifiers
• Higher-order separation logic in Isabelle/HOLCF
• scientific article

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

• 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
• Title not available (Why is that?)
• 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
• Title not available (Why is that?)
• Certification of Automated Termination Proofs
• On the Formalization of Termination Techniques based on Multiset Orderings
• Truly Modular (Co)datatypes for Isabelle/HOL
• Title not available (Why is that?)
• 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
• Title not available (Why is that?)

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

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)