Predrag Janičić ; Filip Marić ; Marko Maliković - Computer-Assisted Proving of Combinatorial Conjectures Over Finite Domains: A Case Study of a Chess Conjecture

lmcs:4233 - Logical Methods in Computer Science, March 29, 2019, Volume 15, Issue 1 - https://doi.org/10.23638/LMCS-15(1:34)2019
Computer-Assisted Proving of Combinatorial Conjectures Over Finite Domains: A Case Study of a Chess ConjectureArticle

Authors: Predrag Janičić ; Filip Marić ; Marko Maliković

    There are several approaches for using computers in deriving mathematical proofs. For their illustration, we provide an in-depth study of using computer support for proving one complex combinatorial conjecture -- correctness of a strategy for the chess KRK endgame. The final, machine verifiable, result presented in this paper is that there is a winning strategy for white in the KRK endgame generalized to $n \times n$ board (for natural $n$ greater than $3$). We demonstrate that different approaches for computer-based theorem proving work best together and in synergy and that the technology currently available is powerful enough for providing significant help to humans deriving complex proofs.


    Volume: Volume 15, Issue 1
    Published on: March 29, 2019
    Accepted on: January 30, 2019
    Submitted on: January 24, 2018
    Keywords: Computer Science - Logic in Computer Science,03B35, 68T15
    Funding:
      Source : OpenAIRE Graph
    • Automated Reasoning and Data Mining; Funder: Ministry of Education, Science and Technological Development of Republic of Serbia; Code: 174021

    Consultation statistics

    This page has been seen 1317 times.
    This article's PDF has been downloaded 633 times.