Pretraga

Pretražite po imenu i prezimenu autora, mentora, urednika, prevoditelja

Napredna pretraga

Pregled bibliografske jedinice broj: 763728

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

Marić, Filip; Janičić, Predrag; Maliković, Marko
Proving Correctness of a KRK Chess Endgame Strategy by using Isabelle/HOL and Z3 // Automated Deduction - CADE-25 / Amy P. Felty and Aart Middeldorp (ur.).
Berlin: Springer, 2015. str. 256-271 doi:10.1007/978-3-319-21401-6_17 (ostalo, recenziran, cjeloviti rad (in extenso), znanstveni)

CROSBI ID: 763728 Za ispravke kontaktirajte CROSBI podršku putem web obrasca

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

Autori
Marić, Filip ; Janičić, Predrag ; Maliković, Marko

Vrsta, podvrsta i kategorija rada
Radovi u zbornicima skupova, cjeloviti rad (in extenso), znanstveni

Izvornik
Automated Deduction - CADE-25 / Amy P. Felty and Aart Middeldorp - Berlin : Springer, 2015, 256-271

ISBN
978-3-319-21401-6

Skup
25th International Conference on Automated Deduction

Mjesto i datum
Berlin, Njemačka, 01.08.2015. - 07.08.2015

Vrsta sudjelovanja
Ostalo

Vrsta recenzije
Recenziran

Ključne riječi
Proving ; KRK ; Strategy ; Isabelle/HOL ; Z3

Sažetak
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.

Izvorni jezik
Engleski

Znanstvena područja
Računarstvo, Informacijske i komunikacijske znanosti



POVEZANOST RADA

Ustanove:
Filozofski fakultet, Rijeka

Profili:

Avatar Url Marko Maliković (autor)

Poveznice na cjeloviti tekst rada:

doi link.springer.com

Citiraj ovu publikaciju:

Marić, Filip; Janičić, Predrag; Maliković, Marko
Proving Correctness of a KRK Chess Endgame Strategy by using Isabelle/HOL and Z3 // Automated Deduction - CADE-25 / Amy P. Felty and Aart Middeldorp (ur.).
Berlin: Springer, 2015. str. 256-271 doi:10.1007/978-3-319-21401-6_17 (ostalo, recenziran, cjeloviti rad (in extenso), znanstveni)
Marić, F., Janičić, P. & Maliković, M. (2015) Proving Correctness of a KRK Chess Endgame Strategy by using Isabelle/HOL and Z3. U: Amy P. Felty and Aart Middeldorp (ur.)Automated Deduction - CADE-25 doi:10.1007/978-3-319-21401-6_17.
@article{article, author = {Mari\'{c}, Filip and Jani\v{c}i\'{c}, Predrag and Malikovi\'{c}, Marko}, year = {2015}, pages = {256-271}, DOI = {10.1007/978-3-319-21401-6\_17}, keywords = {Proving, KRK, Strategy, Isabelle/HOL, Z3}, doi = {10.1007/978-3-319-21401-6\_17}, isbn = {978-3-319-21401-6}, title = {Proving Correctness of a KRK Chess Endgame Strategy by using Isabelle/HOL and Z3}, keyword = {Proving, KRK, Strategy, Isabelle/HOL, Z3}, publisher = {Springer}, publisherplace = {Berlin, Njema\v{c}ka} }
@article{article, author = {Mari\'{c}, Filip and Jani\v{c}i\'{c}, Predrag and Malikovi\'{c}, Marko}, year = {2015}, pages = {256-271}, DOI = {10.1007/978-3-319-21401-6\_17}, keywords = {Proving, KRK, Strategy, Isabelle/HOL, Z3}, doi = {10.1007/978-3-319-21401-6\_17}, isbn = {978-3-319-21401-6}, title = {Proving Correctness of a KRK Chess Endgame Strategy by using Isabelle/HOL and Z3}, keyword = {Proving, KRK, Strategy, Isabelle/HOL, Z3}, publisher = {Springer}, publisherplace = {Berlin, Njema\v{c}ka} }

Časopis indeksira:


  • Web of Science Core Collection (WoSCC)
    • Conference Proceedings Citation Index - Science (CPCI-S)
  • Scopus

Citati:

    Altmetrijski pokazatelji:


    Podijeli:





    Contrast
    Increase Font
    Decrease Font
    Dyslexic Font
    CROSBI koristi kolačiće (cookies) kako bi poboljšao funkcionalnost stranice.