Verifying Faradžev-Read Type Isomorph-Free Exhaustive Generation

DOI10.1007/978-3-030-51054-1_16MaRDI QIDQ5049007zbMATH OpenOpenAlexFDO

Authors Filip Marić

Publication date 9 November 2022

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-030-51054-1_16

zbMATH Keywords

orderlyIsabelle/HOLsoftware verificationisomorph-free exhaustive generation

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• scientific article; zbMATH DE number 3639629 (Why is no real title available?)
• A verified algorithm enumerating event structures
• Every one a Winner or how to Avoid Isomorphism Search when Cataloguing Combinatorial Configurations
• Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points
• Flyspeck I: Tame Graphs
• Formalizing Frankl's conjecture: FC-families
• Generation of union-closed sets and Moore families
• Group actions, double cosets, and homomorphisms: Unifying concepts for the constructive theory of discrete structures
• Imperative Functional Programming with Isabelle/HOL
• Isabelle/HOL. A proof assistant for higher-order logic
• Isomorph-Free Exhaustive Generation
• Refinement to imperative HOL
• The journey of the union-closed sets conjecture
• Verified efficient enumeration of plane graphs modulo isomorphism

Cited in

(2)

• A proof system for graph (non)-isomorphism verification
• Faradžev Read-type enumeration of non-isomorphic CC systems

Describes a project that uses

Uses Software

• Archive Formal Proofs
• Refinement Monadic
• Flyspeck
• Isabelle/HOL

This page was built for publication: Verifying Faradžev-Read Type Isomorph-Free Exhaustive Generation

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