| 1. |
- 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.
|
|
| 2. |
- 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.
|
|
| 3. |
- 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.
|
|
| 4. |
|
|
| 5. |
- Szalas, Andrzej
(författare)
-
On Natural Deduction in First-Order Fixpoint Logics
- 1996
-
Ingår i: Fundamenta Informaticae. - : IOS Press. - 0169-2968 .- 1875-8681. ; 26:1, s. 81-94
-
Tidskriftsartikel (refereegranskat)abstract
- In the current paper we present a powerful technique of obtaining natural deduction proof systems for first-order fixpoint logics. The term fixpoint logics refers collectively to a class of logics consisting of modal logics with modalities definable at meta-level by fixpoint equations on formulas. The class was found very interesting as it contains most logics of programs with e.g. dynamic logic, temporal logic and the ¯-calculus among them. In this paper we present a technique that allows us to derive automatically natural deduction systems for modal logics from fixpoint equations defining the modalities
|
|
