A proof system for graph (non)-isomorphism verification

DOI10.46298/lmcs-19(1:9)2023OpenAlexW4318817948MaRDI QIDQ5883756

Unnamed Author, Milan Banković, Filip Marić

Publication date: 22 March 2023

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2112.14303v5

zbMATH Keywords

interactive theorem provingformal proof systemgraph canonical labellinggraph isomorphism checkingnon-isomorphism certifying

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Uses Software

• nauty
• Sledgehammer
• Traces
• DRAT-trim
• kepler98
• conauto

Cites Work

• Unnamed Item
• Unnamed Item
• Certifying algorithms
• Introduction to ``Milestones in interactive theorem proving
• Practical graph isomorphism. II.
• Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
• Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Formalization of Abstract State Transition Systems for SAT
• Solving SAT and SAT Modulo Theories
• Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
• The Four Colour Theorem: Engineering of a Formal Proof
• Isomorph-Free Exhaustive Generation
• Verifying Faradžev-Read Type Isomorph-Free Exhaustive Generation
• Extending Sledgehammer with SMT Solvers
• A FORMAL PROOF OF THE KEPLER CONJECTURE
• Efficient verified (UN)SAT certificate checking