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

DOI10.1007/978-3-030-51054-1_16OpenAlexW3040328713MaRDI QIDQ5049007

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

orderlysoftware verificationIsabelle/HOLisomorph-free exhaustive generation

Mathematics Subject Classification ID

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

Related Items

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

Uses Software

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

Cites Work

• Unnamed Item
• Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points
• The journey of the union-closed sets conjecture
• Group actions, double cosets, and homomorphisms: Unifying concepts for the constructive theory of discrete structures
• Isabelle/HOL. A proof assistant for higher-order logic
• Refinement to imperative HOL
• A verified algorithm enumerating event structures
• Formalizing Frankl’s Conjecture: FC-Families
• Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism
• Imperative Functional Programming with Isabelle/HOL
• Flyspeck I: Tame Graphs
• Every one a Winner or how to Avoid Isomorphism Search when Cataloguing Combinatorial Configurations
• Isomorph-Free Exhaustive Generation
• Generation of Union Closed Sets and Moore families