Permutative logic (PL) is a noncommutative variant of multiplicative linear logic (MLL) arising from recent investigations concerning the topology of linear proofs. Permutative sequents are structured as oriented surf...
详细信息
ISBN:
(纸本)9783540755586
Permutative logic (PL) is a noncommutative variant of multiplicative linear logic (MLL) arising from recent investigations concerning the topology of linear proofs. Permutative sequents are structured as oriented surfaces with boundary whose topological complexity is able to encode some information about the exchange in sequential proofs. In this paper we provide a complete permutative sequent calculus by extending that one of PL with rules for additives and exponentials. this extended system, here called permutative linear logic (PLL), is shown to be a conservative extension of linear logic and able to enjoy cut-elimination. Moreover, some basic isomorphisms are pointed out.
In this talk we discuss what, according to my long experience, every computer scientists should know from logic. We concentrate on issues of modelling, interpretability and levels of abstraction. We discuss how the mi...
详细信息
Integrating description logics (DL) and logicprogramming (LP) would produce a very powerful and useful formalism. However, DLs and LP are based on quite different principles, so achieving a seamless integration is no...
详细信息
Integrating description logics (DL) and logicprogramming (LP) would produce a very powerful and useful formalism. However, DLs and LP are based on quite different principles, so achieving a seamless integration is not trivial. In this paper, we introduce hybrid MKNF knowledge bases that faithfully integrate DLs with LP using the logic of Minimal Knowledge and Negation as Failure (MKNF) [Lifschitz, 1991]. We also give reasoning algorithms and tight data complexity bounds for several interesting fragments of our logic.
Nonmonotonic causal logic, invented by McCain and Turner, is a formalism well suited for representing knowledge about actions, and the definite fragment of that formalism has been implemented in the reasoning and plan...
详细信息
Nonmonotonic causal logic, invented by McCain and Turner, is a formalism well suited for representing knowledge about actions, and the definite fragment of that formalism has been implemented in the reasoning and planning system called CCalc. A 1997 theorem due to McCain shows how to translate definite causal theories into logicprogramming under the answer set semantics, and thus opens the possibility of using answer set programming for the implementation of such theories. In this paper we propose a generalization of McCain's theorem that extends it in two directions. First, it is applicable to arbitrary causal theories, not only definite. Second, it covers causal theories of a more general kind, which can describe non-Boolean fluents.
We investigate the possibility of developing a decidable logic which allows expressing a large variety of real world specifications. the idea is to define a decidable subset of many-sorted (typed) first- order logic. ...
详细信息
ISBN:
(纸本)9783540755586
We investigate the possibility of developing a decidable logic which allows expressing a large variety of real world specifications. the idea is to define a decidable subset of many-sorted (typed) first- order logic. the motivation is that types simplify the complexity of mixed quantifiers when they quantify over different types. We noticed that many real world verification problems can be formalized by quantifying over different types in such a way that the relations between types remain simple. Our main result is a decidable fragment of many-sorted first-order logicthat captures many real world specifications.
Uncertain information is present in many real applications e.g., medical domain, weather forecast, etc. the most common approaches for leading withthis information are based on probability however some times;it is di...
详细信息
ISBN:
(纸本)9783540766308
Uncertain information is present in many real applications e.g., medical domain, weather forecast, etc. the most common approaches for leading withthis information are based on probability however some times;it is difficult to find suitable probabilities about some events. In this paper, we present a possibilistic logicprogramming approach which is based on possibilistic logic and PStable semantics. Possibilistic logic is a logic of uncertainty tailored for reasoning under incomplete evidence and Pstable Semantics is a solid semantics which emerges from the fusion of non-monotonic reasoning and logicprogramming;moreover it is able to express answer set semantics, and has strong connections with paraconsistent logics.
Current Answer Set programming systems are built on nonmonotonic logic programs without function symbols;as well-known, they lead to high undecidability in general. However, function symbols are highly desirable for v...
详细信息
ISBN:
(纸本)9783540755586
Current Answer Set programming systems are built on nonmonotonic logic programs without function symbols;as well-known, they lead to high undecidability in general. However, function symbols are highly desirable for various applications, which challenges to find meaningful and decidable fragments of this setting. We present the class FDNC of logic programs which allows for function symbols, disjunction, nonmonotonic negation under answer set semantics, and constraints, while still retaining the decidability of the standard reasoning tasks. thanks to these features, they are a powerful formalism for rule-based modeling of applications with potentially infinite processes and objects, which allows also for common-sense reasoning. We show that consistency checking and brave reasoning are EXPTIME-complete in general, but have lower complexity for restricted fragments, and outline worst-case optimal reasoning procedures for these tasks. Furthermore, we present a finite representation of the possibly infinitely many infinite stable models of an FDNC program, which may be exploited for knowledge compilation purposes.
We present a model checking algorithm for HFL1, the first-order fragment of Higher-Order Fixpoint logic. this logic is capable of expressing many interesting properties which are not regular and, hence, not expressibl...
详细信息
ISBN:
(纸本)9783540755586
We present a model checking algorithm for HFL1, the first-order fragment of Higher-Order Fixpoint logic. this logic is capable of expressing many interesting properties which are not regular and, hence, not expressible in the modal mu-calculus. the algorithm avoids best-case exponential behaviour by localising the computation of functions and can be implemented symbolically using BDDs. We show how insight into the behaviour of this procedure, when run on a fixed formula, can be used to obtain specialised algorithms for particular problems. this yields, for example, the competitive antichain algorithm for NFA universality but also a new algorithm for a string matching problem.
We present Zenon, an automated theorem prover for first order classical logic (with equality), based on the tableau method. Zenon is intended to be the dedicated prover of the Focal environment, an object-oriented alg...
详细信息
ISBN:
(纸本)9783540755586
We present Zenon, an automated theorem prover for first order classical logic (with equality), based on the tableau method. Zenon is intended to be the dedicated prover of the Focal environment, an object-oriented algebraic specification and proof system, which is able to produce OCaml code for execution and Coq code for certification. Zenon can directly generate Coq proofs (proof scripts or proof terms), which can be reinserted in the Coq specifications produced by Focal. Zenon can also be extended, which makes specific (and possibly local) automation possible in Focal.
Recent research in nonmonotonic logicprogramming under the answer-set semantics focuses on different notions of program equivalence. However, previous results do not address the important classes of stratified progra...
详细信息
Recent research in nonmonotonic logicprogramming under the answer-set semantics focuses on different notions of program equivalence. However, previous results do not address the important classes of stratified programs and its subclass of acyclic (i.e., recursion-free) programs, although they are recognized as important tools for knowledge representation and reasoning. In this paper, we consider such programs, possibly augmented with constraints. Our results show that in the propositional setting, where reasoning is well-known to be polynomial, deciding strong and uniform equivalence is as hard as for arbitrary normal logic programs (and thus coNP-complete), but is polynomial in some restricted cases. Non-ground programs behave similarly. However, exponential lower bounds already hold for small programs (i.e., with constantly many rules). In particular, uniform equivalence is undecidable even for small Horn programs plus a single negative constraint.
暂无评论