Sciweavers

Share
CADE
2015
Springer

Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3

3 years 2 months ago
Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3
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.
Filip Maric, Predrag Janicic, Marko Malikovic
Added 17 Apr 2016
Updated 17 Apr 2016
Type Journal
Year 2015
Where CADE
Authors Filip Maric, Predrag Janicic, Marko Malikovic
Comments (0)
books