Zobrazeno 1 - 10
of 444
pro vyhledávání: '"Voronkov, Andrei"'
Publikováno v:
Automated Deduction - CADE 29. CADE 2023. Lecture Notes in Computer Science, vol 14132. Springer, Cham
We present an automated reasoning framework for synthesizing recursion-free programs using saturation-based theorem proving. Given a functional specification encoded as a first-order logical formula, we use a first-order theorem prover to both establ
Externí odkaz:
http://arxiv.org/abs/2402.18962
Publikováno v:
Principles of Systems Design 2022, Lecture Notes in Computer Science, vol 13660. Springer, Cham
Induction in saturation-based first-order theorem proving is a new exciting direction in the automation of inductive reasoning. In this paper we survey our work on integrating induction directly into the saturation-based proof search framework of fir
Externí odkaz:
http://arxiv.org/abs/2402.18954
This paper attempts to address the question of how best to assure the correctness of saturation-based automated theorem provers using our experience developing the theorem prover Vampire. We describe the techniques we currently employ to ensure that
Externí odkaz:
http://arxiv.org/abs/1704.03391
The theory of finite term algebras provides a natural framework to describe the semantics of functional languages. The ability to efficiently reason about term algebras is essential to automate program analysis and verification for functional or impe
Externí odkaz:
http://arxiv.org/abs/1611.02908
Modern saturation-based Automated Theorem Provers typically implement the superposition calculus for reasoning about first-order logic with or without equality. Practical implementations of this calculus use a variety of literal selections and term o
Externí odkaz:
http://arxiv.org/abs/1604.08055
This work extends the existing MACE-style finite model finding approach to multi-sorted first order logic. This existing approach iteratively assumes increasing domain sizes and encodes the related ground problem as a SAT problem. When moving to the
Externí odkaz:
http://arxiv.org/abs/1604.08040
This paper presents new features recently implemented in the theorem prover Vampire, namely support for first-order logic with a first class boolean sort (FOOL) and polymorphic arrays. In addition to having a first class boolean sort, FOOL also conta
Externí odkaz:
http://arxiv.org/abs/1510.04821
To support reasoning about properties of programs operating with boolean values one needs theorem provers to be able to natively deal with the boolean sort. This way, program properties can be translated to first-order logic and theorem provers can b
Externí odkaz:
http://arxiv.org/abs/1505.01682