Zobrazeno 1 - 10
of 13
pro vyhledávání: '"Julian Parsert"'
We introduce a novel approach to the automated termination analysis of computer programs: we use neural networks to represent ranking functions. Ranking functions map program states to values that are bounded from below and decrease as a program runs
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::425148fb9c6e144eb41427a5ec0131b8
http://arxiv.org/abs/2102.03824
http://arxiv.org/abs/2102.03824
Publikováno v:
Journal of Logic and Computation
Applying machine learning to mathematical terms and formulas requires a suitable representation of formulas that is adequate for AI methods. In this paper, we develop an encoding that allows for logical properties to be preserved and is additionally
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::e61b4ef34134c23cb1e8f07cafc07b8d
Publikováno v:
GCAI
EPiC Series in Computing volume 72
EPiC Series in Computing volume 72
Logical reasoning as performed by human mathematicians involves an intuitive under- standing of terms and formulas. This includes properties of formulas themselves as well as relations between multiple formulas. Although vital, this intuition is miss
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::cfec573b6a499a33eebf6ff1e5405af8
https://doi.org/10.29007/18t1
https://doi.org/10.29007/18t1
Autor:
Cezary Kaliszyk, Julian Parsert
Publikováno v:
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
Lecture Notes in Computer Science-Interactive Theorem Proving
Interactive Theorem Proving ISBN: 9783319948201
ITP
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Interactive Theorem Proving
Utility functions form an essential part of game theory and economics. In order to guarantee the existence of these utility functions sufficient properties are assumed in an axiomatic manner. In this paper we discuss these axioms and the von-Neumann-
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::0710aa91449a561f695e4e2e9e5cb6c6
Autor:
Julian Parsert, Cezary Kaliszyk
Publikováno v:
Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs-CPP 2018
Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs
CPP
Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs
CPP
Economic activity has always been a fundamental part of society. With recent social and political changes economics has gained even more influence on our lives. In this paper we formalize two economic models in Isabelle/HOL: the pure exchange economy
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::1330685acff7dbe5ec867e945ea1fa64
https://doi.org/10.1145/3176245.3167100
https://doi.org/10.1145/3176245.3167100
Publikováno v:
Interactive Theorem Proving ISBN: 9783319948201
ITP
ITP
In this work we are interested in minimal complete sets of solutions for homogeneous linear diophantine equations. Such equations naturally arise during AC-unification—that is, unification in the presence of associative and commutative symbols. Min
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::1e97efd25409b9656254aafb4058fb89
https://doi.org/10.1007/978-3-319-94821-8_26
https://doi.org/10.1007/978-3-319-94821-8_26
Autor:
Julian Parsert, Yutaka Nagashima
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783319968117
CICM
CICM
We present PGT, a Proof Goal Transformer for Isabelle/HOL. Given a proof goal and its background context, PGT attempts to generate conjectures from the original goal by transforming the original proof goal. These conjectures should be weak enough to
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::0513119d8e613436e34e9f51b0cfe285
https://doi.org/10.1007/978-3-319-96812-4_19
https://doi.org/10.1007/978-3-319-96812-4_19
Publikováno v:
Journal of Logic & Computation; Dec2021, Vol. 31 Issue 8, p2057-2083, 27p
Autor:
Kaliszyk, Cezary, Pąk, Karol
Publikováno v:
Journal of Automated Reasoning; Oct2019, Vol. 63 Issue 3, p557-595, 39p
Publikováno v:
Journal of Logic & Computation; Dec2021, Vol. 31 Issue 8, p1901-1902, 2p