A meta-program is a program that generates or manipulates another program;in homogeneous meta-programming, a program may generate new parts of, or manipulate, itself. Meta-programming has been used extensively since m...
详细信息
ISBN:
(纸本)9783642175107
A meta-program is a program that generates or manipulates another program;in homogeneous meta-programming, a program may generate new parts of, or manipulate, itself. Meta-programming has been used extensively since macros were introduced to Lisp, yet we have little idea how formally to reason about meta-programs. this paper provides the first program logics for homogeneous meta-programming - using a variant of MiniML(e)(square) by Davies and Pfenning as underlying meta-programming language. We show the applicability of our approach by reasoning about example meta-programs from the literature. We also demonstrate that our logics are relatively complete in the sense of Cook, enable the inductive derivation of characteristic formulae, and exactly capture the observational properties induced by the operational semantics.
Standard game theory models implicitly assume that all significant aspects of a game (payoffs, moves available, etc.) are common knowledge among the players. there are well-known techniques going back to Harsanyi [4] ...
详细信息
We introduce pairwise cardinality networks, networks of comparators, derived from pairwise sorting networks, which express cardinality constraints. We show that pairwise cardinality networks are superior to the cardin...
详细信息
ISBN:
(纸本)9783642175107
We introduce pairwise cardinality networks, networks of comparators, derived from pairwise sorting networks, which express cardinality constraints. We show that pairwise cardinality networks are superior to the cardinality networks introduced in previous work which are derived from odd-even sorting networks. Our presentation identifies the precise relationship between odd-even and pairwise sorting networks. this relationship also clarifies why pairwise sorting networks have significantly better propagation properties for the application of cardinality constraints.
We present a sound and complete model of lambda-calculus reductions based on structures inspired by modal logic (closely related to Kripke structures). Accordingly we can construct a logic which is sound and complete ...
详细信息
ISBN:
(纸本)9783642175107
We present a sound and complete model of lambda-calculus reductions based on structures inspired by modal logic (closely related to Kripke structures). Accordingly we can construct a logic which is sound and complete for the same models, and we identify lambda-terms with certain simple sentences (predicates) in this logic, by direct compositional translation. Reduction then becomes identified withlogical entailment. thus, the models suggest a new way to identify logic and computation. Both have elementary and concrete representations in our models;where these representations overlap, they coincide. In a concluding speculation, we note a certain subclass of the models which seems to play a role analogous to that played by the cumulative hierarchy models in axiomatic set theory and the natural numbers in formal arithmetic - there are many models of the respective theories, but only some, characterised by a fully second order interpretation, are the 'intended' ones.
We introduce the method of clausal graph tableaux at the example of hybrid logic with difference and star modalities. Clausal graph tableaux are prefix-free and terminate by construction. they provide an abstract meth...
详细信息
ISBN:
(纸本)9783642162411
We introduce the method of clausal graph tableaux at the example of hybrid logic with difference and star modalities. Clausal graph tableaux are prefix-free and terminate by construction. they provide an abstract method of establishing the small model property of modal logics. In contrast to the filtration method, clausal graph tableaux result in goal-directed decision procedures. Until now no goal-directed decision procedure for the logic considered in this paper was known. there is the promise that clausal graph tableaux lead to a new class of effective decision procedures.
We present an explicitly typed lambda calculus "a la Church" based on the union and intersection types discipline;this system is the counterpart of the standard type assignment calculus "a la Curry.&quo...
详细信息
ISBN:
(纸本)9783642175107
We present an explicitly typed lambda calculus "a la Church" based on the union and intersection types discipline;this system is the counterpart of the standard type assignment calculus "a la Curry." Our typed calculus enjoys the Subject Reduction and Church-Rosser properties, and typed terms are strongly normalizing when the universal type is omitted. Moreover both type checking and type reconstruction are decidable. In contrast to other typed calculi, a system with union types will fail to be "coherent" in the sense of Tannen, Coquand, Gunter, and Scedrov: different proofs of the same typing judgment will not necessarily have the same meaning. In response, we introduce a decidable notion of equality on type-assignment derivations inspired by the equational theory of bicartesian-closed categories.
By Courcelle's theorem we know that any property of finite structures definable in monadic second-order logic (MSO) becomes tractable over structures with bounded treewidth. this result was extended to counting pr...
详细信息
ISBN:
(纸本)9783642175107
By Courcelle's theorem we know that any property of finite structures definable in monadic second-order logic (MSO) becomes tractable over structures with bounded treewidth. this result was extended to counting problems by Arnborg et al. and to enumeration problems by Flum et al. Despite the undisputed importance of these results for proving fixed-parameter tractability, they do not directly yield implementable algorithms. Recently, Gottlob et al. presented a new approach using monadic datalog to close the gap between theoretical tractability and practical computability for MSO-definable decision problems. In the current work we show how counting and enumeration problems can be tackled by an appropriate extension of the datalog approach.
We give a calculus of proof-nets for classical propositional logic. these nets improve on a proposal due to Robinson by validating the associativity and commutativity of contraction, and provide canonical representant...
详细信息
ISBN:
(纸本)9783642162411
We give a calculus of proof-nets for classical propositional logic. these nets improve on a proposal due to Robinson by validating the associativity and commutativity of contraction, and provide canonical representants for classical sequent proofs modulo natural equivalences. We present the relationship between sequent proofs and proof-nets as an annotated sequent calculus, deriving formulae decorated with expansion/deletion trees. We then show a subcalculus, expansion nets, which in addition to these good properties has a polynomial-time correctness criterion.
We present FCUBE, a theorem prover for Intuitionistic propositional logic based on a tableau calculus. the main novelty of FCUBE is that it implements several optimization techniques that allow to prune the search spa...
详细信息
ISBN:
(纸本)9783642162411
We present FCUBE, a theorem prover for Intuitionistic propositional logic based on a tableau calculus. the main novelty of FCUBE is that it implements several optimization techniques that allow to prune the search space acting on different aspects of proof-search. We tested the efficiency of our techniques by comparing FCUBE with other theorem provers. We found that our prover outperforms the other provers on several interesting families of formulas.
We introduce a generic extension of the popular branching-time logic CTL which refines the temporal until and release operators with formal languages. For instance, a language may determine the moments along a pathth...
详细信息
ISBN:
(纸本)9783642162411
We introduce a generic extension of the popular branching-time logic CTL which refines the temporal until and release operators with formal languages. For instance, a language may determine the moments along a paththat an until property may be fulfilled. We consider several classes of languages leading to logics with different expressive power and complexity, whose importance is motivated by their use in model checking, synthesis, abstract interpretation, etc. We show that even with context-free languages on the until operator the logic still allows for polynomial time model-checking despite the significant increase in expressive power. this makes the logic a promising candidate for applications in verification. In addition, we analyse the complexity of satisfiability and compare the expressive power of these logics to CTL* and extensions of PDL.
暂无评论