| 1. |
- Alferes, José Júlio, et al.
(författare)
-
Preface
- 2019
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - 1611-3349 .- 0302-9743. ; 11372 LNCS, s. V-VI
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)
|
|
| 2. |
|
|
| 3. |
- Arvidsson, Andreas, et al.
(författare)
-
Proving Type Class Laws for Haskell
- 2019
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 10447 LNCS, s. 61-74
-
Konferensbidrag (refereegranskat)abstract
- Type classes in Haskell are used to implement ad-hoc polymorphism, i.e. a way to ensure both to the programmer and the compiler that a set of functions are defined for a specific data type. All instances of such type classes are expected to behave in a certain way and satisfy laws associated with the respective class. These are however typically just stated in comments and as such, there is no real way to enforce that they hold. In this paper we describe a system which allows the user to write down type class laws which are then automatically instantiated and sent to an inductive theorem prover when declaring a new instance of a type class.
|
|
| 4. |
- Bonacina, M.P., et al.
(författare)
-
Interpolation Systems for Ground Proofs in Automated Deduction: a Survey
- 2015
-
Ingår i: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 54:4, s. 353-390
-
Tidskriftsartikel (refereegranskat)abstract
- Interpolation is a deductive technique applied in program analysis and verification: for example, it is used to compute over-approximations of images or refine abstractions. An interpolation system takes a refutation and extracts an interpolant by building it inductively from partial interpolants. We survey color-based interpolation systems for ground proofs produced by key inference engines of state-of-the-art solvers: DPLL for propositional logic, equality sharing for combination of convex theories, and DPLL((Formula presented.)) for SMT-solving. Since color-based interpolation systems use colors to track symbols in proofs, equality is problematic, because replacement of equals by equals mixes symbols and therefore colors. We analyze interpolation in the presence of equality, and we demonstrate the color-based approach by giving a complete interpolation system for ground proofs by superposition.
|
|
| 5. |
- Bonacina, M.P., et al.
(författare)
-
On Interpolation in Automated Theorem Proving
- 2015
-
Ingår i: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 54:1, s. 69-97
-
Tidskriftsartikel (refereegranskat)abstract
- Given two inconsistent formul', a (reverse) interpolant is a formula implied by one, inconsistent with the other, and only containing symbols they share. Interpolation finds application in program analysis, verification, and synthesis, for example, towards invariant generation. An interpolation system takes a refutation of the inconsistent formul' and extracts an interpolant by building it inductively from partial interpolants. Known interpolation systems for ground proofs use colors to track symbols. We show by examples that the color-based approach cannot handle non-ground refutations by resolution and paramodulation/superposition. We present a two-stage approach that works by tracking literals, computes a provisional interpolant, which may contain non-shared symbols, and applies lifting to replace non-shared constants by quantified variables. We obtain an interpolation system for non-ground refutations, and we prove that it is complete, if the only non-shared symbols in provisional interpolants are constants.
|
|
| 6. |
- Bundy, A., et al.
(författare)
-
The Theory behind TheoryMine
- 2015
-
Ingår i: IEEE Intelligent Systems. - 1541-1672. ; 30:4, s. 64-69
-
Tidskriftsartikel (refereegranskat)abstract
- The Theory Mine novelty gift company sells the rights to name novel mathematical theorems. The technology is made up of a pipeline of four computer systems that generates recursive theories, then speculates conjectures in those theories and proves the conjectures. All stages of the theorem discovery and proof processes are completely automatic. The process guarantees large numbers of sound, novel theorems of some intrinsic merit.
|
|
| 7. |
- Einarsdóttir, Sólrún, 1991, et al.
(författare)
-
Into the infinite - theory exploration for coinduction
- 2018
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 11110 LNAI, s. 70-86
-
Konferensbidrag (refereegranskat)abstract
- Theory exploration is a technique for automating the discovery of lemmas in formalizations of mathematical theories, using testing and automated proof techniques. Automated theory exploration has previously been successfully applied to discover lemmas for inductive theories, about recursive datatypes and functions. We present an extension of theory exploration to coinductive theories, allowing us to explore the dual notions of corecursive datatypes and functions. This required development of new methods for testing infinite values, and for proof automation. Our work has been implemented in the Hipster system, a theory exploration tool for the proof assistant Isabelle/HOL.
|
|
| 8. |
- Ivarsson, Oscar, 1988, et al.
(författare)
-
Towards Machine Learning on Data from Professional Cyclists
- 2018
-
Ingår i: Proceedings of the XII World Congress of Performance Analysis of Sport. ; 2018
-
Konferensbidrag (refereegranskat)abstract
- Professional sports are developing towards increasingly scientific training methods with increasing amounts of data being collected from laboratory tests, training sessions and competitions. In cycling, it is standard to equip bicycles with small computers recording data from sensors such as power-meters, in addition to heart-rate, speed, altitude etc. Recently, machine learning techniques have provided huge success in a wide variety of areas where large amounts of data (“big data”) is available. In this paper, we perform a pilot experiment on machine learning to model physical response in elite cyclists. As a first experiment, we show that it is possible to train a LSTM machine learning algorithm to predict the heart-rate response of a cyclist during a training session. This work is a promising first step towards developing more elaborate models based on big data and machine learning to capture performance aspects of athletes.
|
|
| 9. |
- Johansson, Moa, 1981
(författare)
-
Automated theory exploration for interactive theorem proving: An introduction to the hipster system
- 2017
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 10499 LNCS, s. 1-11
-
Konferensbidrag (refereegranskat)abstract
- Theory exploration is a technique for automatically discovering new interesting lemmas in a mathematical theory development using testing. In this paper I will present the theory exploration system Hipster, which automatically discovers and proves lemmas about a given set of datatypes and functions in Isabelle/HOL. The development of Hipster was originally motivated by attempts to provide a higher level of automation for proofs by induction. Automating inductive proofs is tricky, not least because they often need auxiliary lemmas which themselves need to be proved by induction. We found that many such basic lemmas can be discovered automatically by theory exploration, and importantly, quickly enough for use in conjunction with an interactive theorem prover without boring the user.
|
|
| 10. |
- Johansson, Moa, 1981, et al.
(författare)
-
Conditional Lemma Discovery and Recursion Induction in Hipster.
- 2015
-
Ingår i: Electronic Communications of the EASST. - 1863-2122. ; 72
-
Tidskriftsartikel (refereegranskat)abstract
- Hipster is a theory exploration tool for the proof assistant Isabelle/HOL. It automatically discovers lemmas about given recursive functions and datatypes and proves them by induction. Previously, only equational properties could be discovered. Conditional lemmas, for example required when reasoning about sorting, has been beyond the scope of theory exploration. In this paper we describe an extension to Hipster to also support discovery and proof of conditional lemmas.We also present a new automated tactic, which uses recursion induction. Recursion induction follows the recursive structure of a function definition through its termina- tion order, as opposed to structural induction, which follows that of the datatype. We find that the addition of recursion induction increases the number of proofs completed automatically, both for conditional and equational statements.
|
|
