1,721,015 research outputs found
Verified Given Clause Procedures
Full text linkResolution and superposition provers rely on the given clause procedure to saturate clause sets. Using Isabelle/HOL, we formally verify four variants of the procedure: the well-known Otter and DISCOUNT loops as well as the newer iProver and Zipperposition loops. For each of the variants, we show that the procedure guarantees saturation, given a fair data structure to store the formulas that wait to be selected. Our formalization of the Zipperposition loop clarifies some fine points previously misunderstood in the literature
Theory Learning with Symmetry Breaking
Full text linkThis paper investigates the use of a Prolog coded SMT solver in tackling a well known constraints problem, namely packing a given set of consecutive squares into a given rectangle, and details the developments in the solver that this motivates. The packing problem has a natural model in the theory of quantifier-free integer difference logic, a theory supported by many SMT solvers. The solver used in this work exploits a data structure consisting of an incremental Floyd-Warshall matrix paired with a watch matrix that monitors the entailment status of integer difference constraints. It is shown how this structure can be used to build unsatisfiable theory cores on the fly, which in turn allows theory learning to be incorporated into the solver. Further, it is shown that a problem-specific and non-standard approach to learning can be taken where symmetry breaking is incorporated into the learning stage, magnifying the effect of learning. It is argued that the declarative framework allows the solver to be used in this white box manner and is a strength of the solver. The approach is experimentally evaluated
A verification technique for deterministic parallel programs
Full text linkSoftware is omnipresent, and software failures can have tremendous costs for society and economy. Therefore, we need techniques to improve the quality of software, and to prevent software failures. Program verification can help to improve this situation, as it allows to check properties on all possible behaviours of a program. We focus in particular on the verification of concurrent software, which is even more error-prone, because of the possible interleavings between the different threads
Automated Deduction – CADE 29
Full text linkThis open access book constitutes the proceedings of the 29th International Conference on Automated Deduction, CADE 29, which took place in Rome, Italy, during July 2023. The 28 full papers and 5 short papers presented were carefully reviewed and selected from 77 submissions. CADE is the major forum for the presentation of research in all aspects of automated deduction, including foundations, applications, implementations, and practical experience. The papers are organized in the following topics: Logical foundations; theory and principles; implementation and application; ATP and AI; and system descriptions
Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic⋆
No full textWe are interested in widening the reasoning support for propositional modal logics in the so-called modal cube. The modal cube consists of extensions of the basic modal logic K with an arbitrary combination of the modal axioms B, D, T, 4 and 5. We revisit recently developed local reductions from all logics in the modal cube to a normal form comprising sets of clausal formulae with associated modal levels. We extend these reductions further to the basic modal logic K, called definitional reductions. This enables any prover for K to be used to solvethe satisfiability problem for all logics in the modal cube.We also presentalternative, axiomatic, reductions based on ideas originally proposed by Kracht, providing new theoretical results and improved bounds on the size of the reductions.We compare both sets of reductions combined with state-of-the-art provers for K on a large set of parametric benchmarks for all logics in the modal cube. The results show that the provers perform better with reductions based on the clausal normal form than the axiomatic reductions
A Compiler for the dependently typed language Beluga
No full textLes structures avec des lieurs sont très communes en informatique. Les langages de programmation et les systèmes logiques sont des exemples de structures avec des lieurs. La manipulation de lieurs est délicate, de sorte que l’écriture de programmes qui ma- nipulent ces structures tirerait profit d’un soutien spécifique pour les lieurs. L’environ- nement de programmation Beluga est un exemple d’un tel système. Nous développons et présentons ici un compilateur pour ce système. Parmi les programmes pour lesquels Beluga est spécialement bien adapté, plusieurs peuvent bénéficier d’un compilateur. Par exemple, les programmes pour valider les types (les "type-checkers"), les compilateurs et les interpréteurs tirent profit du soutien spécifique des lieurs et des types dépendants présents dans le langage. Ils nécessitent tous également une exécution efficace, que l’on propose d’obtenir par le biais d’un compilateur. Le but de ce travail est de présenter un nouveau compilateur pour Beluga, qui emploie une représentation interne polyvalente et permet de partager du code entre plusieurs back-ends. Une contribution notable est la compilation du filtrage de Beluga, qui est particulièrement puissante dans ce langage.In computer science, structures with variable binders are very common. Program- ming languages and logical frameworks are examples of structures with binders. Thus writing programs that deal with these kinds of data benefits with explicit support for data binding. The Beluga programming environment is an example of such a system.
In this work we develop and present a compiler for the system. Many of the programs that Beluga is specially well suited for writing can benefit from a compiler. For example, some of the kinds programs that would benefit more are type-checkers, compilers and interpreters that take advantage of the binder support and dependent types present in the language, and also require a reasonably fast run-time.
Our goal in this work, is to present a compiler for the Beluga system, that uses a very versatile internal representation that helps with the development of the system, and allows a sharing of code between several back-ends. Furthermore, we present a way of compiling the uniquely powerful pattern language supported by Beluga
Expressive and strongly type-safe code generation
No full textMeta-programs are programs that generate other programs, but in weakly type-safe systems, type-checking a meta-program only establishes its own type safety, and generated programs need additional type-checking after generation. Strong type safety of a meta-program implies type safety of any generated object program, a property with important engineering benefits. Current strongly type-safe systems suffer from expressivity limitations and cannot support many meta-programs found in practice, for example automatic generation of lenses.To overcome this, we move away from the idea of staged meta-programming. Instead, we use an off-the-shelf dependently-typed language as the meta-language and a relatively standard, intrinsically well-typed representation of the object language. We scale this approach to practical meta-programming, by choosing a high-level, explicitly typed intermediate representation as the object language, rather than a surface programming language. We implement our approach as a library for the Glasgow Haskell Compiler (GHC) and evaluate it on several meta-programs, including a deriveLenses meta-program taken from a real-world Haskell lens library. Our evaluation demonstrates expressivity beyond the state of the art and applicability to real settings, at little cost in terms of code size.sponsorship: This research is partially funded by the Research Fund KU Leuven and the Agency for Innovation by Science and Technology in Flanders (IWT). Jesper Cockx and Dominique Devriese respectively hold a Ph.D. fellowship and a postdoctoral fellowship of the Research Foundation - Flanders (FWO). (Research Fund KU Leuven, Agency for Innovation by Science and Technology in Flanders (IWT), Research Foundation - Flanders (FWO))status: Publishe
A Compiler for the dependently typed language Beluga
Full text linkLes structures avec des lieurs sont très communes en informatique. Les langages de programmation et les systèmes logiques sont des exemples de structures avec des lieurs. La manipulation de lieurs est délicate, de sorte que l’écriture de programmes qui ma- nipulent ces structures tirerait profit d’un soutien spécifique pour les lieurs. L’environ- nement de programmation Beluga est un exemple d’un tel système. Nous développons et présentons ici un compilateur pour ce système. Parmi les programmes pour lesquels Beluga est spécialement bien adapté, plusieurs peuvent bénéficier d’un compilateur. Par exemple, les programmes pour valider les types (les "type-checkers"), les compilateurs et les interpréteurs tirent profit du soutien spécifique des lieurs et des types dépendants présents dans le langage. Ils nécessitent tous également une exécution efficace, que l’on propose d’obtenir par le biais d’un compilateur. Le but de ce travail est de présenter un nouveau compilateur pour Beluga, qui emploie une représentation interne polyvalente et permet de partager du code entre plusieurs back-ends. Une contribution notable est la compilation du filtrage de Beluga, qui est particulièrement puissante dans ce langage.In computer science, structures with variable binders are very common. Program- ming languages and logical frameworks are examples of structures with binders. Thus writing programs that deal with these kinds of data benefits with explicit support for data binding. The Beluga programming environment is an example of such a system.
In this work we develop and present a compiler for the system. Many of the programs that Beluga is specially well suited for writing can benefit from a compiler. For example, some of the kinds programs that would benefit more are type-checkers, compilers and interpreters that take advantage of the binder support and dependent types present in the language, and also require a reasonably fast run-time.
Our goal in this work, is to present a compiler for the Beluga system, that uses a very versatile internal representation that helps with the development of the system, and allows a sharing of code between several back-ends. Furthermore, we present a way of compiling the uniquely powerful pattern language supported by Beluga
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
- …
