Howe's HOL/Nuprl connection is an interesting example of a translation between two fundamentally different logics, namely a typed higher-order logic and a polymorphic extensional type theory. In earlier work we ha...
详细信息
ISBN:
(纸本)3540482814
Howe's HOL/Nuprl connection is an interesting example of a translation between two fundamentally different logics, namely a typed higher-order logic and a polymorphic extensional type theory. In earlier work we have established a proof-theoretic correctness result of the translation in a way that complements Howe's semantics-based justification and furthermore goes beyond the original HOL/Nuprl connection by providing the foundation for a proof translator. Using the Twelf logical framework, the present paper goes one step further. It presents the first rigorous formalization of this treatment in a logical framework, and hence provides a safe alternative to the translation of proofs.
Recently, LTL extended with atomic formulas built over a constraint language interpreting variables in Z has been shown to have a decidable satisfiability and model-checking problem. this language allows to compare th...
详细信息
ISBN:
(纸本)3540482814
Recently, LTL extended with atomic formulas built over a constraint language interpreting variables in Z has been shown to have a decidable satisfiability and model-checking problem. this language allows to compare the variables at different states of the model and include periodicity constraints, comparison constraints, and a restricted form of quantification. On the other hand, the CTL counterpart of this logic (and hence also its CTL* counterpart which subsumes both LTL and CTL) has an undecidable model-checking problem. In this paper, we substantially extend the decidability border, by considering a meaningful fragment of CTL* extended with such constraints (which subsumes boththe universal and existential fragments, as well as the EF-like fragment) and show that satisfiability and model-checking over relational automata that are abstraction of counter machines are decidable. the correctness and the termination of our algorithm rely on a suitable well quasi-ordering defined over the set of variable valuations.
this paper presents systems for first-order intuitionistic logic and several of its extensions in which all the propositional rules are local, in the sense that, in applying the rules of the system, one needs only a f...
详细信息
ISBN:
(纸本)3540482814
this paper presents systems for first-order intuitionistic logic and several of its extensions in which all the propositional rules are local, in the sense that, in applying the rules of the system, one needs only a fixed amount of information about the logical expressions involved. the main source of non-locality is the contraction rules. We show that the contraction rules can be restricted to the atomic ones, provided we employ deep-inference, i.e., to allow rules to apply anywhere inside logical expressions. We further show that the use of deep inference allows for modular extensions of intuitionistic logic to Dummett's intermediate logic LC, Godel logic and classical logic. We present the systems in the calculus of structures, a proof theoretic formalism which supports deep-inference. Cut elimination for these systems are proved indirectly by simulating the cut-free sequent systems, or the hypersequent systems in the cases of Dummett's LC and Godel logic, in the cut free systems in the calculus of structures.
In a previous work, the first author extended to higher-order rewriting and dependent types the use of size annotations in types, a termination proof technique called type or size based termination and initially devel...
详细信息
ISBN:
(纸本)3540482814
In a previous work, the first author extended to higher-order rewriting and dependent types the use of size annotations in types, a termination proof technique called type or size based termination and initially developed for ML-like programs. Here, we go one step further by considering conditional rewriting and explicit quantifications and constraints on size annotations. this allows to describe more precisely how the size of the output of a function depends on the size of its inputs. Hence, we can check the termination of more functions. We first give a general type-checking algorithm based on constraint solving. then, we give a termination criterion with constraints in Presburger arithmetic. To our knowledge, this is the first termination criterion for higher-order conditional rewriting taking into account the conditions in termination.
We show that the concepts of strong and uniform equivalence of logic programs can be generalized to an abstract algebraic setting of operators on complete lattices. Our results imply characterizations of strong and un...
详细信息
We propose a modular, assertion-based system for verification and debugging of large logic programs, together with several interesting models for checking assertions statically in modular programs, each with different...
详细信息
ISBN:
(纸本)3540482814
We propose a modular, assertion-based system for verification and debugging of large logic programs, together with several interesting models for checking assertions statically in modular programs, each with different characteristics and representing different trade-offs. Our proposal is a modular and multivariant extension of our previously proposed abstract assertion checking model and we also report on its implementation in the CiaoPP system. In our approach, the specification of the program, given by a set of assertions, may be partial, instead of the complete specification required by traditional verification systems. Also, the system can deal with properties which cannot always be determined at compile-time. As a result, the proposed system needs to work with safe approximations: all assertions proved correct are guaranteed to be valid and all errors actual errors. the use of modular, context-sensitive static analyzers also allows us to introduce a new distinction between assertions checked in a particular context or checked in general.
Constructing parsimonious phylogenetic trees from species data is a central problem in phylogenetics, and has diverse applications, even outside biology. Many variations of the problem, including the cladistic Camin-S...
详细信息
ISBN:
(纸本)3540482814
Constructing parsimonious phylogenetic trees from species data is a central problem in phylogenetics, and has diverse applications, even outside biology. Many variations of the problem, including the cladistic Camin-Sokal (CCS) version, are NP-complete. We present Answer Set programming (ASP) models for the binary CCS problem, as well as a simpler perfect phylogeny version, along with experimental results of applying the models to biological data. Our contribution is three-fold. First, we solve phylogeny problems which have not previously been tackled by ASP. Second, we report on variants of our CCS model which significantly. affect run time, including the interesting case of making the program "slightly tighter". this version exhibits some of the best performance, in contrast with a tight version of the model which exhibited poor performance. third, we are able to find proven-optimal solutions for larger instances of the CCS problem than the widely used branch-and-bound-based PHYLIP package.
A stable proposal for extending the first-order TPTP (thousands of Problems for theorem Provers) language to higher-order logic, based primarily on lambda-calculus expressions, is presented. the purpose of the system ...
详细信息
ISBN:
(纸本)3540371877
A stable proposal for extending the first-order TPTP (thousands of Problems for theorem Provers) language to higher-order logic, based primarily on lambda-calculus expressions, is presented. the purpose of the system is to facilitate sharing of theorem-proving problems in higher-order logic among many researchers. Design goals are discussed. BNF2, a new specification language, is presented. Unix/Linux scripts translate the specification document into a lex scanner and yacc parser.
this paper proposes an imperative semantics for a logic of actions: through their axiomatisations, actions are interpreted as programs in an imperative programming language. An argument is made for the naturalness of ...
详细信息
暂无评论