Zobrazeno 1 - 10
of 610
pro vyhledávání: '"URBAN, Josef"'
In this work we considerably improve the state-of-the-art SMT solving on first-order quantified problems by efficient machine learning guidance of quantifier selection. Quantifiers represent a significant challenge for SMT and are technically a sourc
Externí odkaz:
http://arxiv.org/abs/2408.14338
In this work, we prove over 3000 previously ATP-unproved Mizar/MPTP problems by using several ATP and AI methods, raising the number of ATP-solved Mizar problems from 75\% to above 80\%. First, we start to experiment with the cvc5 SMT solver which us
Externí odkaz:
http://arxiv.org/abs/2406.17762
Autor:
Blaauwbroek, Lasse, Cerna, David, Gauthier, Thibault, Jakubův, Jan, Kaliszyk, Cezary, Suda, Martin, Urban, Josef
Automated theorem provers and formal proof assistants are general reasoning systems that are in theory capable of proving arbitrarily hard theorems, thus solving arbitrary problems reducible to mathematics and logical reasoning. In practice, such sys
Externí odkaz:
http://arxiv.org/abs/2403.04017
Publikováno v:
Silva Fennica, Vol 51, Iss 4 (2017)
Scots pine ( L.) is a resilient, wide spread species. This paper reports on the xylem and phloem cell formation process, before and after, the species was put under artificial stress by stem girdling. Microcore method was applied to a healthy control
Externí odkaz:
https://doaj.org/article/a0b84bf24ad04785bb4049adcb300ae6
We describe a translation from a fragment of SUMO (SUMO-K) into higher-order set theory. The translation provides a formal semantics for portions of SUMO which are beyond first-order and which have previously only had an informal interpretation. It a
Externí odkaz:
http://arxiv.org/abs/2305.07903
We present a benchmark of 29687 problems derived from the On-Line Encyclopedia of Integer Sequences (OEIS). Each problem expresses the equivalence of two syntactically different programs generating the same OEIS sequence. Such programs were conjectur
Externí odkaz:
http://arxiv.org/abs/2304.02986
Autor:
Jakubův, Jan, Chvalovský, Karel, Goertzel, Zarathustra, Kaliszyk, Cezary, Olšák, Mirek, Piotrowski, Bartosz, Schulz, Stephan, Suda, Martin, Urban, Josef
As a present to Mizar on its 50th anniversary, we develop an AI/TP system that automatically proves about 60\% of the Mizar theorems in the hammer setting. We also automatically prove 75\% of the Mizar theorems when the automated provers are helped b
Externí odkaz:
http://arxiv.org/abs/2303.06686
We introduce a self-learning algorithm for synthesizing programs for OEIS sequences. The algorithm starts from scratch initially generating programs at random. Then it runs many iterations of a self-learning loop that interleaves (i) training neural
Externí odkaz:
http://arxiv.org/abs/2301.11479
Autor:
Piepenbrock, Jelle, Urban, Josef, Korovin, Konstantin, Olšák, Miroslav, Heskes, Tom, Janota, Mikolaš
The appearance of strong CDCL-based propositional (SAT) solvers has greatly advanced several areas of automated reasoning (AR). One of the directions in AR is thus to apply SAT solvers to expressive formalisms such as first-order logic, for which lar
Externí odkaz:
http://arxiv.org/abs/2210.03590