Recently, linear logic has been used to specify sequent calculus proof systems in such a way that the proof search in linear logic can yield proof search in the specified logic. Furthermore, the meta-theory of linear ...
详细信息
ISBN:
(纸本)354030553X
Recently, linear logic has been used to specify sequent calculus proof systems in such a way that the proof search in linear logic can yield proof search in the specified logic. Furthermore, the meta-theory of linear logic can be used to draw conclusions about the specified sequent calculus. For example, derivability of one proof system from another can be decided by a simple procedure that is implemented via bounded logicprogramming-style search. Also, simple and decidable conditions on the linear logic presentation of inference rules, called homogeneous and coherence, can be used to infer that the initial rules can be restricted to atoms and that cuts can be eliminated. In the present paper we introduce Llinda, a logical framework based on linear logic augmented with inference rules for definition (fixed points) and induction. In this way, the above properties can be proved entirely inside the framework. To further illustrate the power of Llinda, we extend the definition of coherence and provide a new, semi-automated proof of cut-elimination for Girard's logic of Unicity (LU).
We introduce HEX programs, which are nonmonotonic logic programs admitting higher-order atoms as well as external atoms, and we extend the well-known answer-set semantics to this class of programs. Higher-order featur...
详细信息
We introduce HEX programs, which are nonmonotonic logic programs admitting higher-order atoms as well as external atoms, and we extend the well-known answer-set semantics to this class of programs. Higher-order features are widely acknowledged as useful for performing meta-reasoning, among other tasks. Furthermore, the possibility to exchange knowledge with external sources in a fully declarative framework such as Answer-Set programming (ASP) is nowadays important, in particular in view of applications in the Semantic Web area. through external atoms, HEX programs can model some important extensions to ASP, and are a useful KR tool for expressing various applications. Finally, complexity and implementation issues for a preliminary prototype are discussed.
the main goal of this paper is to apply rewriting termination technology-enjoying a quite mature set of termination results and tools-to the problem of proving automatically the termination of concurrent systems under...
详细信息
ISBN:
(纸本)354030553X
the main goal of this paper is to apply rewriting termination technology-enjoying a quite mature set of termination results and tools-to the problem of proving automatically the termination of concurrent systems under fairness assumptions. We adopt the thesis that a concurrent system can be naturally modeled as a rewrite system, and develop a reductionistic theoretical approach to systematically transform, under reasonable assumptions, fair-termination problems into ordinary termination problems of associated relations, to which standard rewriting termination techniques and tools can be applied. Our theoretical results are combined into a practical proof methodology for proving fair-termination that can be automated and can be supported by current termination tools. We illustrate this methodology with some concrete examples and briefly comment on future extensions.
CERES is a method for cut-elimination in classical logic which is based on resolution. In this paper we extend CERES to CERES-m, a resolution-based method of cut-elimination in Gentzen calculi for arbitrary finitely-v...
详细信息
ISBN:
(纸本)3540252363
CERES is a method for cut-elimination in classical logic which is based on resolution. In this paper we extend CERES to CERES-m, a resolution-based method of cut-elimination in Gentzen calculi for arbitrary finitely-valued logics. Like in the classical case the core of the method is the construction of a resolution proof in finitely-valued logics. Compared to Gentzen-type cut-elimination methods the advantage of CERES-m is a twofold one: 1. it is easier to define and 2. it is computationally superior and thus more appropriate for implementations and experiments.
We introduce a declarative approach for a coherent composition of autonomous databases. For this we use ID-logic, a formalism that extends classical logic with inductive definitions. We consider ID-logictheories that...
详细信息
ISBN:
(纸本)3540285385
We introduce a declarative approach for a coherent composition of autonomous databases. For this we use ID-logic, a formalism that extends classical logic with inductive definitions. We consider ID-logictheories that express, at the same time, the two basic challenges in database composition problems: relating different schemas of the local databases to one global schema (schema integration) and amalgamating the distributed and possibly contradictory data to one consistent database (data integration). We show that our framework supports different methods for schema integration (as well as their combinations) and that it provides a straightforward way of dealing with inconsistent data. Moreover, this framework facilitates the implementation of database repair and consistent query answering by means of a variety of reasoning systems.
Formal verification methods model systems by Kripke structures. In order to model live behaviors of systems, Kripke structures are augmented with fairness conditions. Such conditions partition the computations of the ...
详细信息
ISBN:
(纸本)3540252363
Formal verification methods model systems by Kripke structures. In order to model live behaviors of systems, Kripke structures are augmented with fairness conditions. Such conditions partition the computations of the systems into fair computations, with respect to which verification proceeds, and unfair computations, which are ignored. reasoning about Kripke structures augmented with fairness is typically harder than reasoning about non-fair Kripke structures. We consider the transition fairness condition, where a computation pi is fair iff each transition that is enabled in pi infinitely often is also taken in pi infinitely often. Transition fairness is a natural and useful fairness condition. We show that reasoning about Kripke structures augmented with transition fairness is not harder than reasoning about non-fair Kripke structures. We demonstrate it for fair CTL and LTL model checking, and the problem of calculating the dominators and postdominators.
We observe, that subsumption of clauses (in the language of first order logic), so far understood as a syntactic notion, can also be defined by semantical means. Subsumption is NP-complete and testing subsumption take...
详细信息
ISBN:
(纸本)3540252363
We observe, that subsumption of clauses (in the language of first order logic), so far understood as a syntactic notion, can also be defined by semantical means. Subsumption is NP-complete and testing subsumption takes roughly half of the running time of a typical first order resolution-based theorem prover. We also give some experimental evidence, that replacing syntactic indexing for subsumption by our semantic Monte Carlo technique can, in some situations, significantly decrease the cost of subsumption. testing. Finally, we provide some evidence that a similar semantic idea can be probably successfully used for testing for AC matching, which is another NP-complete problem whose millions of instances are being solved by theorem provers.
In this work we describe a system for determining strong equivalence of disjunctive non-ground datalog programs under the stable model semantics. the problem is tackled by reducing it to the unsatisfiability problem o...
详细信息
ISBN:
(纸本)3540285385
In this work we describe a system for determining strong equivalence of disjunctive non-ground datalog programs under the stable model semantics. the problem is tackled by reducing it to the unsatisfiability problem of first-order formulas in the Bernays-Schonfinkel fragment. We then employ a tableaux-based theorem prover, which (unlike most other currently available provers) is guaranteed to terminate for these formulas. To the best of our knowledge, this is the first strong equivalence tester for disjunctive non-ground datalog.
Within the setting of object-oriented program specification and verification, pointers and object references can be considered as relations between the elements of a data structure. When we specify properties of these...
详细信息
ISBN:
(纸本)354030553X
Within the setting of object-oriented program specification and verification, pointers and object references can be considered as relations between the elements of a data structure. When we specify properties of these data structures, we often describe properties of relations. Hence it is important to be able to talk about relations and their properties when specifying object-oriented programs or programs with pointers. Many interesting properties of relations such as transitive closure, finiteness, and generatedness are not expressible in first-order logic (FOL);hence neither are they expressible in first-order fragments of specification languages. In this paper we give an overview of the different ways such properties can be expressed in various logics, with a particular emphasis on extensions of FOL, i.e. transitive closure logic, fixed-point logic, and first-order dynamic logic. Within the paper we also discuss which of these extensions already are - or in fact should be - implemented within specification languages. We feel that such a discussion is necessary since it is often the case that when an extension of FOL is implemented within a specification language it is done so in an ad hoc manner or the underpinning logical concepts are not well documented.
the traditional purpose of types in programming languages of providing correctness assurances at compile time is increasingly being supplemented by a direct role for them in the computational process. In the context o...
详细信息
ISBN:
(纸本)354030553X
the traditional purpose of types in programming languages of providing correctness assurances at compile time is increasingly being supplemented by a direct role for them in the computational process. In the context of typed logicprogramming, this is manifest in their effect on the unification operation. their influence takes two different forms. First, in a situation where polymorphism is permitted, type information is needed to determine if different occurrences of the same name in fact denote an identical constant. Second, type information may determine the form of bindings for variables. When types are needed for the second purpose as in the case of higher-order unification, these have to be available with every variable and constant. However, in situations such as first-order and higher-order pattern unification, types have no impact on the variable binding process. As a consequence, type examination is needed in these situations only for the first of the two purposes described and even here a careful preprocessing can considerably reduce their run-time footprint. We develop a scheme for treating types in these contexts that exploits this observation. Under this scheme, type information is elided in most cases and is embedded into term structure when this is not entirely possible. Our approach obviates types when properties known as definitional genericity and type preservation are satisfied and has the advantage of working even when these conditions are violated.
暂无评论