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 23, 2024
Google ScholarTM
Check
Altmetric
Altmetric
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.