| 1. |
- Abrahamsson, Oskar, 1986, et al.
(author)
-
Proof-Producing Synthesis of CakeML from Monadic HOL Functions
- 2020
-
In: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 64:7, s. 1287-1306
-
Journal article (peer-reviewed)abstract
- We introduce an automatic method for producing stateful ML programs together with proofs of correctness from monadic functions in HOL. Our mechanism supports references, exceptions, and I/O operations, and can generate functions manipulating local state, which can then be encapsulated for use in a pure context. We apply this approach to several non-trivial examples, including the instruction encoder and register allocator of the otherwise pure CakeML compiler, which now benefits from better runtime performance. This development has been carried out in the HOL4 theorem prover.
|
|
| 2. |
- Ahrens, B., et al.
(author)
-
From Signatures to Monads in UniMath
- 2019
-
In: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 63:2, s. 285-318
-
Journal article (peer-reviewed)abstract
- The term UniMath refers both to a formal system for mathematics, as well as a computer-checked library of mathematics formalized in that system. The UniMath system is a core dependent type theory, augmented by the univalence axiom. The system is kept as small as possible in order to ease verification of it-in particular, general inductive types are not part of the system. In this work, we partially remedy the lack of inductive types by constructing some set-level datatypes and their associated induction principles from other type constructors. This involves a formalization of a category-theoretic result on the construction of initial algebras, as well as a mechanism to conveniently use the datatypes obtained. We also connect this construction to a previous formalization of substitution for languages with variable binding. Altogether, we construct a framework that allows us to concisely specify, via a simple notion of binding signature, a language with variable binding. From such a specification we obtain the datatype of terms of that language, equipped with a certified monadic substitution operation and a suitable recursion scheme. Using this we formalize the untyped lambda calculus and the raw syntax of Martin-Lof type theory.
|
|
| 3. |
|
|
| 4. |
- Bengtson, Jesper, et al.
(author)
-
Psi-Calculi in Isabelle
- 2016
-
In: Journal of automated reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 56:1, s. 1-47
-
Journal article (peer-reviewed)abstract
- This paper presents a mechanisation of psi-calculi, a parametric framework for modelling various dialects of process calculi including (but not limited to) the pi-calculus, the applied pi-calculus, and the spi calculus. psi-calculi are significantly more expressive, yet their semantics is as simple in structure as the semantics of the original pi-calculus. Proofs of meta-theoretic properties for psi-calculi are more involved, however, not least because psi-calculi (unlike simpler calculi) utilise binders that bind multiple names at once. The mechanisation is carried out in the Nominal Isabelle framework, an interactive proof assistant designed to facilitate formal reasoning about calculi with binders. Our main contributions are twofold. First, we have developed techniques that allow efficient reasoning about calculi that bind multiple names in Nominal Isabelle. Second, we have adopted these techniques to mechanise substantial results from the meta-theory of psi-calculi, including congruence properties of bisimilarity and the laws of structural congruence. To our knowledge, this is the most extensive formalisation of process calculi mechanised in a proof assistant to date.
|
|
| 5. |
- Bezem, M., et al.
(author)
-
The Univalence Axiom in Cubical Sets
- 2019
-
In: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 63:2, s. 159-171
-
Journal article (peer-reviewed)abstract
- In this note we show that Voevodsky's univalence axiom holds in the model of type theory based on cubical sets as described inBezem et al. (in: Matthes and Schubert (eds.) 19th international conference on types for proofs and programs (TYPES 2013), Leibniz international proceedings in informatics (LIPIcs), Schloss Dagstuhl-Leibniz-Zentrum fur Informatik, Dagstuhl, Germany, vol26, pp 107-128, 2014. 10.4230/LIPIcs.TYPES.2013.107. http://drops.dagstuhl.de/opus/volltexte/2014/4628) and Huber (A model of type theory in cubical sets. Licentiate thesis, University of Gothenburg, 2015). We will also discuss Swan's construction of the identity type in this variation of cubical sets. This proves that we have a model of type theory supporting dependent products, dependent sums, univalent universes, and identity types with the usual judgmental equality, and this model is formulated in a constructive metatheory.
|
|
| 6. |
- Birkedal, Lars, et al.
(author)
-
Guarded Cubical Type Theory
- 2019
-
In: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 63:2, s. 211-253
-
Journal article (peer-reviewed)abstract
- This paper improves the treatment of equality in guarded dependent type theory ((Formula presented.)), by combining it with cubical type theory ((Formula presented.)). (Formula presented.) is an extensional type theory with guarded recursive types, which are useful for building models of program logics, and for programming and reasoning with coinductive types. We wish to implement (Formula presented.) with decidable type checking, while still supporting non-trivial equality proofs that reason about the extensions of guarded recursive constructions. (Formula presented.) is a variation of Martin–Löf type theory in which the identity type is replaced by abstract paths between terms. (Formula presented.) provides a computational interpretation of functional extensionality, enjoys canonicity for the natural numbers type, and is conjectured to support decidable type-checking. Our new type theory, guarded cubical type theory ((Formula presented.)), provides a computational interpretation of extensionality for guarded recursive types. This further expands the foundations of (Formula presented.) as a basis for formalisation in mathematics and computer science. We present examples to demonstrate the expressivity of our type theory, all of which have been checked using a prototype type-checker implementation. We show that (Formula presented.) can be given semantics in presheaves on (Formula presented.), where (Formula presented.) is the cube category, and (Formula presented.) is any small category with an initial object. We then show that the category of presheaves on (Formula presented.) provides semantics for (Formula presented.).
|
|
| 7. |
- Björk, Magnus, 1977
(author)
-
First Order Stålmarck
- 2009
-
In: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 42:1, s. 99-122
-
Journal article (peer-reviewed)abstract
- We present a proof method with a novel way of introducing universal lemmas. The method is a first order extension of StAyenlmarck's method, containing a branch-and-merge rule known as the dilemma rule. The dilemma rule creates two branches in a tableau-like way, but later recombines the two branches, keeping the common consequences. While the propositional version uses normal set intersection in the merges, the first order version searches for pairwise unifiable formulae in the two branches. Within branches, the system uses a special kind of variables that may not be substituted. At branch merges, these variables are replaced by universal variables, and in this way universal lemmas can be introduced. Relevant splitting formulae are found through failed unifications of variables in branches. This article presents the calculus and proof procedure, and shows soundness and completeness. Benchmarks of an implementation are also presented.
|
|
| 8. |
- Bonacina, M.P., et al.
(author)
-
Interpolation Systems for Ground Proofs in Automated Deduction: a Survey
- 2015
-
In: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 54:4, s. 353-390
-
Journal article (peer-reviewed)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.
|
|
| 9. |
- Bonacina, M.P., et al.
(author)
-
On Interpolation in Automated Theorem Proving
- 2015
-
In: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 54:1, s. 69-97
-
Journal article (peer-reviewed)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.
|
|
| 10. |
- Brillout, Angelo, et al.
(author)
-
An interpolating sequent calculus for quantifier-free Presburger arithmetic
- 2011
-
In: Journal of automated reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 47:4, s. 341-367
-
Journal article (peer-reviewed)abstract
- Craig interpolation has become a versatile tool in formal verification, used for instance to generate program assertions that serve as candidates for loop invariants. In this paper, we consider Craig interpolation for quantifier-free Presburger arithmetic (QFPA). Until recently, quantifier elimination was the only available interpolation method for this theory, which is, however, known to be potentially costly and inflexible. We introduce an interpolation approach based on a sequent calculus for QFPA that determines interpolants by annotating the steps of an unsatisfiability proof with partial interpolants. We prove our calculus to be sound and complete. We have extended the Princess theorem prover to generate interpolating proofs, and applied it to a large number of publicly available Presburger arithmetic benchmarks. The results document the robustness and efficiency of our interpolation procedure. Finally, we compare the procedure against alternative interpolation methods, both for QFPA and linear rational arithmetic.
|
|
| 11. |
- Claessen, Koen, 1975, et al.
(author)
-
Handling Transitive Relations in First-Order Automated Reasoning
- 2021
-
In: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 65:8, s. 1097-1124
-
Journal article (peer-reviewed)abstract
- We present a number of alternative ways of handling transitive binary relations that commonly occur in first-order problems, in particular equivalence relations, total orders, and transitive relations in general. We show how such relations can be discovered syntactically in an input theory, and how they can be expressed in alternative ways. We experimentally evaluate different such ways on problems from the TPTP, using resolution-based reasoning tools as well as instance-based tools. Our conclusions are that (1) it is beneficial to consider different treatments of binary relations as a user, and that (2) reasoning tools could benefit from using a preprocessor or even built-in support for certain types of binary relations.
|
|
| 12. |
- Cok, David R., et al.
(author)
-
The 2013 Evaluation of SMT-COMP and SMT-LIB
- 2015
-
In: Journal of automated reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 55:1, s. 61-90
-
Journal article (peer-reviewed)abstract
- After 8 years of SMT Competitions, the SMT Steering Committee decided, for 2013, to sponsor an evaluation of the status of SMT benchmarks and solvers, rather than another competition. This report summarizes the results of the evaluation, conducted by the authors. The key observations are that (1) the competition results are quite sensitive to randomness and (2) the most significant need for the future is assessment and improvement of benchmarks in the light of SMT applications. The evaluation also measured competitiveness of solvers, general coverage of solvers, logics, and benchmarks, and degree of repeatability of measurements and competitions.
|
|
| 13. |
- Davis, J., et al.
(author)
-
The Reflective Milawa Theorem Prover is Sound (Down to the Machine Code that Runs it)
- 2015
-
In: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 55:2, s. 117-183
-
Journal article (peer-reviewed)abstract
- This paper presents, we believe, the most comprehensive evidence of a theorem prover’s soundness to date. Our subject is the Milawa theorem prover. We present evidence of its soundness down to the machine code. Milawa is a theorem prover styled after NQTHM and ACL2. It is based on an idealised version of ACL2’s computational logic and provides the user with high-level tactics similar to ACL2’s. In contrast to NQTHM and ACL2, Milawa has a small kernel that is somewhat like an LCF-style system. We explain how the Milawa theorem prover is constructed as a sequence of reflective extensions from its kernel. The kernel establishes the soundness of these extensions during Milawa’s bootstrapping process. Going deeper, we explain how we have shown that the Milawa kernel is sound using the HOL4 theorem prover. In HOL4, we have formalized its logic, proved the logic sound, and proved that the source code for the Milawa kernel (1,700 lines of Lisp) faithfully implements this logic. Going even further, we have combined these results with the x86 machine-code level verification of the Lisp runtime Jitawa. Our top-level theorem states that Milawa can never claim to prove anything that is false when it is run on this Lisp runtime.
|
|
| 14. |
- Doherty, Patrick, 1957-, et al.
(author)
-
Computing circumscription revisited : A reduction algorithm
- 1997
-
In: Journal of automated reasoning. - : Kluwer Academic Publishers. - 0168-7433 .- 1573-0670. ; 18:3, s. 297-336
-
Journal article (peer-reviewed)abstract
- In recent years, a great deal of attention has been devoted to logics of common-sense reasoning. Among the candidates proposed, circumscription has been perceived as an elegant mathematical technique for modeling nonmonotonic reasoning, but difficult to apply in practice. The major reason for this is the second-order nature of circumscription axioms and the difficulty in finding proper substitutions of predicate expressions for predicate variables. One solution to this problem is to compile, where possible, second-order formulas into equivalent first-order formulas. Although some progress has been made using this approach, the results are not as strong as one might desire and they are isolated in nature. In this article, we provide a general method that can be used in an algorithmic manner to reduce certain circumscription axioms to first-order formulas. The algorithm takes as input an arbitrary second-order formula and either returns as output an equivalent first-order formula, or terminates with failure. The class of second-order formulas, and analogously the class of circumscriptive theories that can be reduced, provably subsumes those covered by existing results. We demonstrate the generality of the algorithm using circumscriptive theories with mixed quantifiers (some involving Skolemization), variable constants, nonseparated formulas, and formulas with n-ary predicate variables. In addition, we analyze the strength of the algorithm, compare it with existing approaches, and provide formal subsumption results.
|
|
| 15. |
- Huber, Simon, 1984
(author)
-
Canonicity for Cubical Type Theory
- 2019
-
In: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 63:2, s. 173-210
-
Journal article (peer-reviewed)abstract
- Cubical type theory is an extension of Martin-Lof type theory recently proposed by Cohen, Coquand, Mortberg, and the author which allows for direct manipulation of n-dimensional cubes and where Voevodsky's Univalence Axiom is provable. In this paper we prove canonicity for cubical type theory: any natural number in a context build from only name variables is judgmentally equal to a numeral. To achieve this we formulate a typed and deterministic operational semantics and employ a computability argument adapted to a presheaf-like setting.
|
|
| 16. |
- Kamareddine, F., et al.
(author)
-
Formalizing strong normalization proofs of explicit substitution calculi in ALF
- 2003
-
In: Journal of Automated Reasoning. - 0168-7433 .- 1573-0670. ; 30:1, s. 59-98
-
Journal article (peer-reviewed)abstract
- The past decade has given rise to a number of explicit substitution calculi. An important question of explicit substitution calculi is that of the termination of the underlying calculus of substitution. Proofs of termination of substitutions fall in two categories: those that are easy because a decreasing measure can be established and those that are difficult because such a decreasing measure is not easy to establish. This paper considers two styles of explicit substitution: σ and s, for which different termination proof methods apply. The termination of s is guaranteed by a decreasing weight, while a decreasing weight for showing the termination of σ has not yet been found. These termination methods for σ and s are formalized in the proof checker ALF. During our process of formally checking the termination of σ and s we comment on what is needed to make a proof formally checkable.
|
|
| 17. |
- Kumar, R., et al.
(author)
-
Self-Formalisation of Higher-Order Logic Semantics, Soundness, and a Verified Implementation
- 2016
-
In: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 56:3, s. 221-259
-
Journal article (peer-reviewed)abstract
- We present a mechanised semantics for higher-order logic (HOL), and a proof of soundness for the inference system, including the rules for making definitions, implemented by the kernel of the HOL Light theorem prover. Our work extends Harrison's verification of the inference system without definitions. Soundness of the logic extends to soundness of a theorem prover, because we also show that a synthesised implementation of the kernel in CakeML refines the inference system. Apart from adding support for definitions and synthesising an implementation, we improve on Harrison's work by making our model of HOL parametric on the universe of sets, and we prove soundness for an improved principle of constant specification in the hope of encouraging its adoption. Our semantics supports defined constants directly via a context, and we find this approach cleaner than our previous work formalising Wiedijk's Stateless HOL.
|
|
| 18. |
- Lindström Claessen, Koen, 1975, et al.
(author)
-
Automated Inference of Finite Unsatisfiability
- 2011
-
In: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 47:2, s. 111-132
-
Journal article (peer-reviewed)abstract
- We present Infinox, an automated tool for analyzing first-order logic problems, aimed at showing finite unsatisfiability, i.e., the absence of models with finite domains. Finite satisfiability is not a decidable problem (only semi-decidable), which means that such a tool can never be complete. Nonetheless, our hope is that Infinox be a useful complement to finite model finders in practice. Infinox uses several different proof techniques for showing infinity of a set, each of which requires the identification of a function or a relation with particular properties. Infinox enumerates candidates to such functions and relations, and subsequently uses an automated theorem prover as a sub-procedure to try to prove the resulting proof obligations. We have evaluated Infinox on the relevant problems from the TPTP benchmark suite, and we are able to automatically show finite unsatisfiability for over 25% of these problems.
|
|
| 19. |
- Sandberg Eriksson, Adam, 1991, et al.
(author)
-
A Verified Generational Garbage Collector for CakeML
- 2019
-
In: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 63:2, s. 463-488
-
Journal article (peer-reviewed)abstract
- This paper presents the verification of a generational copying garbage collector for the CakeML runtime system. The proof is split into an algorithm proof and an implementation proof. The algorithm proof follows the structure of the informal intuition for the generational collector’s correctness, namely, a partial collection cycle in a generational collector is the same as running a full collection on part of the heap, if one views pointers to old data as non-pointers. We present a pragmatic way of dealing with ML-style mutable state, such as references and arrays, in the proofs. The development has been fully integrated into the in-logic bootstrapped CakeML compiler, which now includes command-line arguments that allow configuration of the generational collector. All proofs were carried out in the HOL4 theorem prover.
|
|
| 20. |
|
|
| 21. |
- Degtyarev, A, et al.
(author)
-
What you always wanted to know about rigid E-unification
- 1998
-
In: JOURNAL OF AUTOMATED REASONING. - : KLUWER ACADEMIC PUBL. - 0168-7433. ; 20:1-2, s. 47-80
-
Journal article (other academic/artistic)abstract
- This paper solves an open problem posed by a number of researchers: the construction of a complete calculus for matrix-based methods with rigid E-unification. The use of rigid E-unification and simultaneous rigid E-unification for such methods was propose
|
|
| 22. |
- Voronkov, A
(author)
-
Proof search in intuitionistic logic with equality, or back to simultaneous rigid E-unification
- 1998
-
In: JOURNAL OF AUTOMATED REASONING. - : KLUWER ACADEMIC PUBL. - 0168-7433. ; 21:2, s. 205-231
-
Journal article (other academic/artistic)abstract
- We characterize provability in intuitionistic logic with equality in terms of a constraint calculus. This characterization uncovers close connections between provability in intuitionistic logic with equality and solutions to simultaneous rigid E-unificati
|
|
| 23. |
- VORONKOV, A
(author)
-
THE ANATOMY OF VAMPIRE
- 1995
-
In: JOURNAL OF AUTOMATED REASONING. - : KLUWER ACADEMIC PUBL. - 0168-7433. ; 15:2, s. 237-265
-
Journal article (other academic/artistic)abstract
- We present an implementation technique for a class of bottom-up logic procedures. The technique is based on code trees. It is intended to speed up most important and costly operations, such as subsumption and resolution. As an example, we consider the for
|
|
| 24. |
- Krupic, Ferid, et al.
(author)
-
The Influence of Age, Gender and Religion on Willingness to be an Organ Donor: Experience of Religious Muslims Living in Sweden.
- 2019
-
In: Journal of religion and health. - : Springer Science and Business Media LLC. - 1573-6571 .- 0022-4197. ; 58, s. 847-859
-
Journal article (peer-reviewed)abstract
- The transplantation of organs is one of the most successful medical advances in recent decades, and transplantation is the treatment of choice for severe organ failure worldwide. Despite this situation and the general acknowledgment of organ donation (OD) as a global priority, the demand for organs outstrips the supply in virtually every country in the world. The study aims to elucidate whether age, gender and religion influence decision-making about organ donation in religious Muslims living in Sweden Data were collected through three group interviews using open-ended questions and qualitative content analysis. Twenty-seven participants, 15 males and 12 females from four countries, participated in the focus group interviews. The analysis of the collected data resulted in three main categories: "Information and knowledge about organ donation," "The priorities when deciding about organ donation" and "The religious aspects of organ donation," including a number of subcategories. Good information about and knowledge of OD, priorities in OD, importance of the fact that religion must be studied and taught daily and religious education were only a few of the factors informants emphasized as predictors of the total and successful donation of organs. Age, gender or religion did not have an impact on organ donation. High levels of education through religious education and good information via various media, as well as a good knowledge of the Swedish language, are predictors of improved OD. In order to overcome religious ideology as a source of misinformation relating to OD and to promote increased OD in the future, specific intervention studies and the improved involvement of religious communities and education in schools and the healthcare system are vital and must be a starting point for improved OD.
|
|
