| 1. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Monotonic and downward closed games
- 2008
-
Ingår i: Journal of logic and computation (Print). - : Oxford University Press (OUP). - 0955-792X .- 1465-363X. ; 18:1, s. 153-169
-
Tidskriftsartikel (refereegranskat)abstract
- In an earlier work [Abdulla et al. (2000, Information and Computation, 160, 109127)] we presented a general framework for verification of infinite-state transition systems, where the transition relation is monotonic with respect to a well quasi-ordering on the set of states. In this article, we investigate extending the framework from the context of transition systems to that of games with infinite state spaces. We show that monotonic games with safety winning conditions are in general undecidable. In particular, we show this negative results for games which are defined over Petri nets. We identify a subclass of monotonic games, called downward closed games. We provide algorithms for analysing downward closed games subject to safety winning conditions. We apply the algorithm to games played on lossy channel systems. Finally, we show that weak parity games are undecidable for the above classes of games.
|
|
| 2. |
- Bodirsky, Manuel, et al.
(författare)
-
Horn versus Full First-order : Complexity Dichotomies in Algebraic Constraint Satisfaction
- 2012
-
Ingår i: Journal of logic and computation (Print). - : Oxford University Press (OUP). - 0955-792X .- 1465-363X. ; 22:3, s. 643-660
-
Tidskriftsartikel (refereegranskat)abstract
- We study techniques for deciding the computational complexity of infinite-domain constraint satisfaction problems. For certain fundamental algebraic structures Delta, we prove definability dichotomy theorems of the following form: for every first-order expansion Gamma of Delta, either Gamma has a quantifier-free Horn definition in Delta, or there is an element d of Gamma such that all non-empty relations in Gamma contain a tuple of the form (d,...,d), or all relations with a first-order definition in Delta have a primitive positive definition in Gamma. The results imply that several families of constraint satisfaction problems exhibit a complexity dichotomy: the problems are in P or NP-hard, depending on the choice of the allowed relations. As concrete examples, we investigate fundamental algebraic constraint satisfaction problems. The first class consists of all first-order expansions of (Q;+). The second class is the affine variant of the first class. In both cases, we obtain full dichotomies by utilising our general methods.
|
|
| 3. |
- Boella, Guido, et al.
(författare)
-
Introduction to the special issue on NorMAS 2009
- 2013
-
Ingår i: Journal of logic and computation (Print). - : Oxford University Press (OUP). - 0955-792X .- 1465-363X. ; 23:2, s. 307-308
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)
|
|
| 4. |
- Boldrin, Luca, et al.
(författare)
-
A modal logic for fusing partial belief of multiple reasoners
- 1999
-
Ingår i: Journal of logic and computation (Print). - : Oxford University Press (OUP). - 0955-792X .- 1465-363X. ; 9:1, s. 81-103
-
Tidskriftsartikel (refereegranskat)abstract
- We present PLn, a multi-agent epistemic logic in which each agent can perform uncertain (possibilistic) reasoning. The original feature of this logic is the presence of a distributed belief operator, with the purpose of merging the belief of different agents. Unlike the corresponding operator in the categorical (non-uncertain) case, our distributed belief operator accumulates support for the same fact coming from different agents. This means that opinions shared by different agents can be combined into a stronger distributed belief. This feature is useful in problems like pooling expert opinions and combining information from multiple unreliable sources. We provide a possible worlds semantics and an axiomatic calculus for our logic, and prove soundness, completeness and decidability results. We hint at some possible applications of PLn in the conclusions
|
|
| 5. |
- Creignou, Nadia, et al.
(författare)
-
Complexity classifications for propositional abduction in Post's framework
- 2012
-
Ingår i: Journal of logic and computation (Print). - : Oxford University Press (OUP). - 0955-792X .- 1465-363X. ; 22:5, s. 1145-1170
-
Tidskriftsartikel (refereegranskat)abstract
- In this article, we investigate the complexity of abduction, a fundamental and important form of non-monotonic reasoning. Given a knowledge base explaining the world's behaviour, it aims at finding an explanation for some observed manifestation. In this article, we consider propositional abduction, where the knowledge base and the manifestation are represented by propositional formulæ. The problem of deciding whether there exists an explanation has been shown to be Σ2p-complete in general. We focus on formulæ in which the allowed connectives are taken from certain sets of Boolean functions. We consider different variants of the abduction problem in restricting both the manifestations and the hypotheses. For all these variants, we obtain a complexity classification for all possible sets of Boolean functions. In this way, we identify easier cases, namely NP-complete, coNP-complete and polynomial cases. Thus, we get a detailed picture of the complexity of the propositional abduction problem, hence highlighting the sources of intractability. Further, we address the problem of counting the full explanations and prove a trichotomous classification theorem.
|
|
| 6. |
- Dahlgren, Fredrik
(författare)
-
Partial Continuous Functions and Admissible Domain Representations
- 2007
-
Ingår i: Journal of logic and computation (Print). - : Oxford University Press (OUP). - 0955-792X .- 1465-363X. ; 17:6, s. 1063-1081
-
Tidskriftsartikel (refereegranskat)abstract
- It is well known that to be able to represent continuous functions between domain representable spaces it is critical that the domain representations of the spaces we consider are dense. In this article we show how to develop a representation theory over a category of domains with morphisms partial continuous functions. The raison detre for introducing partial continuous functions is that by passing to partial maps, we are free to consider totalities which are not dense. We show that the category of admissibly representable spaces with morphisms functions which are representable by it partial continuous function is Cartesian closed. Finally, we consider the question of effectivity.
|
|
| 7. |
- Dam, Mads, et al.
(författare)
-
mu-calculus with explicit points and approximations
- 2002
-
Ingår i: Journal of logic and computation (Print). - : Oxford University Press (OUP). - 0955-792X .- 1465-363X. ; 12:2, s. 255-269
-
Tidskriftsartikel (refereegranskat)abstract
- We present a Gentzen-style sequent calculus for program verification which accommodates both model checking-like verification based on global state space exploration, and compositional reasoning. To handle the complexities arising from the presence of fixed-point formulas, programs with dynamically evolving architecture, and cut rules we use transition assertions, and introduce fixed-point approximants explicitly into the assertion language. We address, in a game-based manner, the semantical basis of this approach, as it applies to the entailment subproblem. Soundness and completeness results are obtained, and examples are shown illustrating some of the concepts.
|
|
| 8. |
- Doherty, Patrick, 1957-, et al.
(författare)
-
Declarative PTIME queries for relational databases using quantifier elimination
- 1999
-
Ingår i: Journal of logic and computation (Print). - : Oxford University Press. - 0955-792X .- 1465-363X. ; 9:5, s. 737-758
-
Tidskriftsartikel (refereegranskat)abstract
- In this paper, we consider the problem of expressing and computing queries on relational deductive databases in a purely declarative query language, called SHQL (Semi-Horn Query Language). Assuming the relational databases in question are ordered, we show that all SHQL queries are computable in PTIME (polynomial time) and the whole class of PTIME queries is expressible in SHQL. Although similar results have been proven for fixpoint languages and extensions to datalog, the claim is that SHQL has the advantage of being purely declarative, where the negation operator is interpreted as classical negation, mixed quantifiers may be used and a query is simply a restricted first-order theory not limited by the rule-based syntactic restrictions associated with logic programs in general. We describe the PTIME algorithm used to compute queries in SHQL which is based in part on quantifier elimination techniques and also consider extending the method to incomplete relational databases using intuitions related to circumscription techniques.
|
|
| 9. |
- Douven, Igor, et al.
(författare)
-
From Probabilities to Categorical Beliefs : Going Beyond Toy Models
- 2018
-
Ingår i: Journal of logic and computation (Print). - : Oxford University Press (OUP). - 0955-792X .- 1465-363X. ; 28, s. 1099-1124
-
Tidskriftsartikel (refereegranskat)abstract
- According to the Lockean thesis, a proposition is believed just in case it is highly probable. While this thesis enjoys strong intuitive support, it is known to conflict with seemingly plausible logical constraints on our beliefs. One way out of this conflict is to make probability 1 a requirement for belief, but most have rejected this option for entailing what they see as an untenable skepticism. Recently, two new solutions to the conflict have been proposed that are alleged to be non-skeptical. We compare these proposals with each other and with the Lockean thesis, in particular with regard to the question of how much we gain by adopting any one of them instead of the probability 1 requirement, that is, of how likely it is that one believes more than the things one is fully certain of.
|
|
| 10. |
- Dybjer, Peter, 1953, et al.
(författare)
-
The extended predicative Mahlo universe in Martin-Lof type theory
- 2023
-
Ingår i: Journal of Logic and Computation. - 0955-792X .- 1465-363X. ; In Press
-
Tidskriftsartikel (refereegranskat)abstract
- This paper addresses the long-standing question of the predicativity of the Mahlo universe. A solution, called the extended predicative Mahlo universe, has been proposed by Kahle and Setzer in the context of explicit mathematics. It makes use of the collection of untyped terms (denoting partial functions) which are directly available in explicit mathematics but not in Martin-Lof type theory. In this paper, we overcome the obstacle of not having direct access to untyped terms in Martin-Lof type theory by formalizing explicit mathematics with an extended predicative Mahlo universe in Martin-Lof type theory with certain indexed inductive-recursive definitions. In this way, we can relate the predicativity question to the fundamental semantics of Martin-Lof type theory in terms of computation to canonical form. As a result, we get the first extended predicative definition of a Mahlo universe in Martin-Lof type theory. To this end, we first define an external variant of Kahle and Setzer's internal extended predicative universe in explicit mathematics. This is then formalized in Martin-Lof type theory, where it becomes an internal extended predicative Mahlo universe. Although we make use of indexed inductive-recursive definitions that go beyond the type theory $\mathbf {IIRD}$ of indexed inductive-recursive definitions defined in previous work by the authors, we argue that they are constructive and predicative in Martin-Lof's sense. The model construction has been type-checked in the proof assistant Agda.
|
|
