Proving Correctness of a KRK Chess Endgame Strategy by using Isabelle/HOL and Z3 (CROSBI ID 624588)
Prilog sa skupa u časopisu | izvorni znanstveni rad
Podaci o odgovornosti
Marić, Filip ; Janičić, Predrag ; Maliković, Marko
engleski
Proving Correctness of a KRK Chess Endgame Strategy by using Isabelle/HOL and Z3
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.
Proving ; KRK ; Strategy ; Isabelle/HOL ; Z3
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
Podaci o prilogu
256-271.
2015.
nije evidentirano
objavljeno
10.1007/978-3-319-21401-6_17
Podaci o matičnoj publikaciji
Lecture notes in computer science
Amy P. Felty and Aart Middeldorp
Berlin: Springer
978-3-319-21401-6
0302-9743
1611-3349
Podaci o skupu
25th International Conference on Automated Deduction
ostalo
01.08.2015-07.08.2015
Berlin, Njemačka
Povezanost rada
Informacijske i komunikacijske znanosti, Računarstvo