| 1. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Universality Analysis for One-Clock Timed Automata
- 2008
-
Ingår i: Fundamenta Informaticae. - 0169-2968 .- 1875-8681. ; 89:4, s. 419-450
-
Tidskriftsartikel (refereegranskat)abstract
- This paper is concerned with the universality problem for timed automata: given a timed automaton A, does A accept all timed words? Alur and Dill have shown that the universality problem is undecidable if A has two clocks, but they left open the status of the problem when A has a single clock. In this paper we close this gap for timed automata over infinite words by showing that the one-clock universality problem is undecidable. For timed automata over finite words we show that the one-clock universality problem is decidable with non-primitive recursive complexity. This reveals a surprising divergence between the theory of timed automata over finite words and over infinite words. We also show that if epsilon-transitions or non-singular postconditions are allowed, then the one-clock universality problem is undecidable over both finite and infinite words. Furthermore, we present a zone-based algorithm for solving the universality problem for single-clock timed automata. We apply the theory of better quasi-orderings, a refinement of the theory of well quasi-orderings, to prove termination of the algorithm. We have implemented a prototype tool based on our method, and checked universality for a number of timed automata. Comparisons with a region-based prototype tool confirm that zones are a more succinct representation, and hence allow a much more efficient implementation of the universality algorithm.
|
|
| 2. |
|
|
| 3. |
|
|
| 4. |
- Bezem, M., et al.
(författare)
-
Skolem's Theorem in Coherent Logic
- 2019
-
Ingår i: Fundamenta Informaticae. - : IOS Press. - 0169-2968 .- 1875-8681. ; 170:1-3, s. 1-14
-
Tidskriftsartikel (refereegranskat)abstract
- We give a constructive proof of Skolem's Theorem for coherent logic and discuss several applications, including a negative answer to a question by Wraith.
|
|
| 5. |
- Cattani, Carlo, et al.
(författare)
-
On the Critical Strip of the Riemann zeta Fractional derivative
- 2017
-
Ingår i: Fundamenta Informaticae. - 0169-2968 .- 1875-8681. ; 151, s. 459-472
-
Tidskriftsartikel (refereegranskat)abstract
- The fractional derivative of the Dirichlet eta function is computed in order to investigate the behavior of the fractional derivative of the Riemann zeta function on the critical strip. Its convergence is studied. In particular, its half-plane of convergence gives the possibility to better understand the fractional derivative of the Riemann zeta function and its critical strip. As an application, two signal processing networks, corresponding to the fractional derivative of the eta function and to its Fourier transform, respectively, are shortly described.
|
|
| 6. |
- Doherty, Patrick, et al.
(författare)
-
A correspondence framework between three-valued logics and similarity-based approximate reasoning
- 2007
-
Ingår i: Fundamenta Informaticae. - : IOS Press. - 0169-2968 .- 1875-8681. ; 75:1-4, s. 179-193
-
Tidskriftsartikel (refereegranskat)abstract
- This paper focuses on approximate reasoning based on the use of similarity spaces. Similarity spaces and the approximated relations induced by them are a generalization of the rough set-based approximations of Pawlak [17, 18]. Similarity spaces are used to define neighborhoods around individuals and these in turn are used to define approximate sets and relations. In any of the approaches, one would like to embed such relations in an appropriate logic which can be used as a reasoning engine for specific applications with specific constraints. We propose a framework which permits a formal study of the relationship between approximate relations, similarity spaces and three-valued logics. Using ideas from correspondence theory for modal logics and constraints on an accessibility relation, we develop an analogous framework for three-valued logics and constraints on similarity relations. In this manner, we can provide a tool which helps in determining the proper three-valued logical reasoning engine to use for different classes of approximate relations generated via specific types of similarity spaces. Additionally, by choosing a three-valued logic first, the framework determines what constraints would be required on a similarity relation and the approximate relations induced by it. Such information would guide the generation of approximate relations for specific applications.
|
|
| 7. |
- Doherty, Patrick, 1957-, et al.
(författare)
-
A reduction result for circumscribed semi-horn formulas
- 1996
-
Ingår i: Fundamenta Informaticae. - : IOS Press. - 0169-2968 .- 1875-8681. ; 28:3,4, s. 261-272
-
Tidskriftsartikel (refereegranskat)abstract
- Circumscription has been perceived as an elegant mathematical technique for modeling nonmonotonic and commonsense reasoning, but difficult to apply in practice due to the use of second-order formulas. One proposal for dealing with the computational problems is to identify classes of first-order formulas whose circumscription can be shown to be equivalent to a first-order formula. In previous work, we presented an algorithm which reduces certain classes of second-order circumscription axioms to logically equivalent first-order formulas. The basis for the algorithm is an elimination lemma due to Ackermann. In this paper, we capitalize on the use of a generalization of Ackermann's Lemma in order to deal with a subclass of universal formulas called semi-Horn formulas. Our results subsume previous results by Kolaitis and Papadimitriou regarding a characterization of circumscribed definite logic programs which are first-order expressible. The method for distinguishing which formulas are reducible is based on a boundedness criterion. The approach we use is to first reduce a circumscribed semi-Horn formula to a fixpoint formula which is reducible if the formula is bounded, otherwise not. In addition to a number of other extensions, we also present a fixpoint calculus which is shown to be sound and complete for bounded fixpoint formulas.
|
|
| 8. |
- Doherty, Patrick, et al.
(författare)
-
Automated Generation of Logical Constraints on Approximation Spaces Using Quantifier Elimination
- 2013
-
Ingår i: Fundamenta Informaticae. - : IOS Press. - 0169-2968 .- 1875-8681. ; 127:1-4, s. 135-149
-
Tidskriftsartikel (refereegranskat)abstract
- This paper focuses on approximate reasoning based on the use of approximation spaces. Approximation spaces and the approximated relations induced by them are a generalization of the rough set-based approximations of Pawlak. Approximation spaces are used to define neighborhoods around individuals and rough inclusion functions. These in turn are used to define approximate sets and relations. In any of the approaches, one would like to embed such relations in an appropriate logical theory which can be used as a reasoning engine for specific applications with specific constraints. We propose a framework which permits a formal study of the relationship between properties of approximations and properties of approximation spaces. Using ideas from correspondence theory, we develop an analogous framework for approximation spaces. We also show that this framework can be strongly supported by automated techniques for quantifier elimination.
|
|
| 9. |
- Doherty, Patrick, 1957-, et al.
(författare)
-
General domain circumscription and its effective reductions.
- 1998
-
Ingår i: Fundamenta Informaticae. - : IOS Press. - 0169-2968 .- 1875-8681. ; 36:1, s. 23-55
-
Tidskriftsartikel (refereegranskat)abstract
- We first define general domain circumscription (GDC) and provide it with a semantics. GDC subsumes existing domain circumscription proposals in that it allows varying of arbitrary predicates, functions, or constants, to maximize the minimization of the domain of a theory. We then show that for the class of semi-universal theories without function symbols, that the domain circumscription of such theories can be constructively reduced to logically equivalent first-order theories by using an extension of the DLS algorithm, previously proposed by the authors for reducing second-order formulas. We also show that for a certain class of domain circumscribed theories, that any arbitrary second-order circumscription policy applied to these theories is guaranteed to be reducible to a logically equivalent first-order theory. In the case of semi-universal theories with functions and arbitrary theories which are not separated, we provide additional results, which although not guaranteed to provide reductions in all cases, do provide reductions in some cases. These results are based on the use of fixpoint reductions.
|
|
| 10. |
- Doherty, Patrick, 1957-, et al.
(författare)
-
Meta-queries on deductive databases
- 1999
-
Ingår i: Fundamenta Informaticae. - : IOS Press. - 0169-2968 .- 1875-8681. ; 40:1, s. 17-30
-
Tidskriftsartikel (refereegranskat)abstract
- We introduce the notion of a meta-query on relational databases and a technique which can be used to represent and solve a number of interesting problems from the area of knowledge representation using logic. The technique is based on the use of quantifier elimination and may also be used to query relational databases using a declarative query language called SHQL (Semi-Horn Query Language), introduced in [6]. SHQL is a fragment of classical first-order predicate logic and allows us to define a query without supplying its explicit definition. All SHQL queries to the database can be processed in polynomial time (both on the size of the input query and the size of the database). We demonstrate the use of the technique in problem solving by structuring logical puzzles from the Knights and Knaves domain as SHQL meta-queries on relational databases. We also provide additional examples demonstrating the flexibility of the technique. We conclude with a description of a newly developed software tool, The Logic Engineer, which aids in the description of algorithms using transformation and reduction techniques such as those applied in the meta-querying approach.
|
|
