Please use this identifier to cite or link to this item: https://research.matf.bg.ac.rs/handle/123456789/515
Title: Proving correctness of a KRK chess endgame strategy by using isabelle/HOL and Z3
Authors: Marić, Filip 
Janičić, Predrag 
Maliković, Marko
Affiliations: Informatics and Computer Science 
Informatics and Computer Science 
Issue Date: 1-Jan-2015
Related Publication(s): International Conference on Automated Deduction CADE 2015
Journal: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Abstract: 
We describe an executable specification and a total correctness proof of a King and Rook vs King (KRK) chess endgame strategy within the proof assistant Isabelle/HOL. This work builds upon a previous computer-assisted correctness analysis performed using the constraint solver URSA. The distinctive feature of the present machine verifiable formalization is that all central properties have been automatically proved by the SMT solver Z3 integrated into Isabelle/HOL, after being suitably expressed in linear integer arithmetic. This demonstrates that the synergy between the state-of-the-art automated and interactive theorem proving is mature enough so that very complex conjectures from various AI domains can be proved almost in a “push-button” manner, yet in a rich logical framework offered by the modern ITP systems.
URI: https://research.matf.bg.ac.rs/handle/123456789/515
ISSN: 03029743
DOI: 10.1007/978-3-319-21401-6_17
Appears in Collections:Research outputs

Show full item record

SCOPUSTM   
Citations

3
checked on Dec 18, 2024

Page view(s)

23
checked on Dec 24, 2024

Google ScholarTM

Check

Altmetric

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.