Zobrazeno 1 - 6
of 6
pro vyhledávání: '"Zarathustra Goertzel"'
Publikováno v:
Frontiers of Combining Systems ISBN: 9783030862046
FroCoS
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Frontiers of Combining Systems
Frontiers of Combining Systems-13th International Symposium, FroCoS 2021, Birmingham, UK, September 8–10, 2021, Proceedings
FroCoS
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Frontiers of Combining Systems
Frontiers of Combining Systems-13th International Symposium, FroCoS 2021, Birmingham, UK, September 8–10, 2021, Proceedings
We describe several additions to the ENIGMA system that guides clause selection in the E automated theorem prover. First, we significantly speed up its neural guidance by adding server-based GPU evaluation. The second addition is motivated by fast we
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::aa5a8aae68167d5c24056c4bb774a206
https://doi.org/10.1007/978-3-030-86205-3_10
https://doi.org/10.1007/978-3-030-86205-3_10
Autor:
Zarathustra Goertzel
Publikováno v:
Automated Reasoning-10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Automated Reasoning
Automated Reasoning
Automated Reasoning ISBN: 9783030510534
IJCAR (2)
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Automated Reasoning
Automated Reasoning
Automated Reasoning ISBN: 9783030510534
IJCAR (2)
In this work in progress, we demonstrate a new use-case for the ENIGMA system. The ENIGMA system using the XGBoost implementation of gradient boosted decision trees has demonstrated high capability to learn to guide the E theorem prover’s inference
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4712937a59925fa6897437cc3855d486
Publikováno v:
Technological Forecasting and Social Change. 114:65-73
The emergence of artificial general intelligence and the global brain provides new opportunities for realizing humanity's long quest for a more utopian existence. One possibility is a more successful implementation of the state socialist vision of a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f697e87598fbc6ef344fc28886ca6699
https://doi.org/10.1016/j.techfore.2016.03.022
https://doi.org/10.1016/j.techfore.2016.03.022
Publikováno v:
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Automated Reasoning with Analytic Tableaux and Related Methods
Lecture Notes in Computer Science ISBN: 9783030290252
TABLEAUX
Automated Reasoning with Analytic Tableaux and Related Methods-28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings
Lecture Notes in Computer Science-Automated Reasoning with Analytic Tableaux and Related Methods
Lecture Notes in Computer Science ISBN: 9783030290252
TABLEAUX
Automated Reasoning with Analytic Tableaux and Related Methods-28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings
In this work we describe a new learning-based proof guidance – ENIGMAWatch – for saturation-style first-order theorem provers. ENIGMAWatch combines two guiding approaches for the given-clause selection implemented for the E ATP system: ProofWatch
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3c03a49d5723a2ea85d97e881f61111b
Publikováno v:
LPAR (Workshop and Short Papers)
Kalpa Publications in Computing volume 9
Kalpa Publications in Computing volume 9
Watchlist (also hint list) is a technique that allows lemmas from related proofs to guide a saturation-style proof search for a new conjecture. ProofWatch is a recent watchlist-style method that loads many previous proofs inside the ATP, maintains th
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f251394d424839251ecb529e10092d0a
Publikováno v:
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Interactive Theorem Proving
Interactive Theorem Proving-9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings
Interactive Theorem Proving ISBN: 9783319948201
ITP
Lecture Notes in Computer Science-Interactive Theorem Proving
Interactive Theorem Proving-9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings
Interactive Theorem Proving ISBN: 9783319948201
ITP
Watchlist (also hint list) is a mechanism that allows related proofs to guide a proof search for a new conjecture. This mechanism has been used with the Otter and Prover9 theorem provers, both for interactive formalizations and for human-assisted pro
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b1442f3f1754a0f9cd97bb7bfb459581