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

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

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

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

Cited In (2)

• 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

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)