Please use this identifier to cite or link to this item:
https://research.matf.bg.ac.rs/handle/123456789/491
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Janičić, Predrag | en_US |
dc.contributor.author | Marić, Filip | en_US |
dc.contributor.author | Maliković, Marko | en_US |
dc.date.accessioned | 2022-08-13T10:13:44Z | - |
dc.date.available | 2022-08-13T10:13:44Z | - |
dc.date.issued | 2019-01-01 | - |
dc.identifier.uri | https://research.matf.bg.ac.rs/handle/123456789/491 | - |
dc.description.abstract | 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 × 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 some complex proofs. | en_US |
dc.relation.ispartof | Logical Methods in Computer Science | en_US |
dc.subject | Chess | en_US |
dc.subject | chess endgame | en_US |
dc.subject | constraint programming | en_US |
dc.subject | proof assistants | en_US |
dc.subject | SAT | en_US |
dc.subject | SMT | en_US |
dc.subject | strategy | en_US |
dc.subject | theorem proving | en_US |
dc.title | On thin air reads: Towards an event structures model of relaxed memory | en_US |
dc.type | Article | en_US |
dc.identifier.doi | 10.23638/LMCS-15(1:34)2019 | - |
dc.identifier.scopus | 2-s2.0-85070371706 | - |
dc.identifier.url | https://api.elsevier.com/content/abstract/scopus_id/85070371706 | - |
dc.contributor.affiliation | Informatics and Computer Science | en_US |
dc.contributor.affiliation | Informatics and Computer Science | en_US |
dc.relation.lastpage | 34:37 | en_US |
dc.relation.volume | 15 | en_US |
dc.relation.issue | 1 | en_US |
item.fulltext | No Fulltext | - |
item.openairecristype | http://purl.org/coar/resource_type/c_18cf | - |
item.cerifentitytype | Publications | - |
item.grantfulltext | none | - |
item.openairetype | Article | - |
crisitem.author.dept | Informatics and Computer Science | - |
crisitem.author.dept | Informatics and Computer Science | - |
crisitem.author.orcid | 0000-0001-8922-4948 | - |
crisitem.author.orcid | 0000-0001-7219-6960 | - |
Appears in Collections: | Research outputs |
SCOPUSTM
Citations
3
checked on Dec 18, 2024
Page view(s)
13
checked on Dec 24, 2024
Google ScholarTM
Check
Altmetric
Altmetric
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.