| 1. |
- Degtyarev, A, et al.
(författare)
-
A note on semantics of logic programs with equality based on complete sets of E-unifiers
- 1996
-
Ingår i: JOURNAL OF LOGIC PROGRAMMING. - : ELSEVIER SCIENCE INC. - 0743-1066. ; 28:3, s. 207-216
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)abstract
- We discuss semantics of equational Horn-clause programs based on the notion of a complete set of E-unifiers. We prove incompleteness of SLDE dagger-resolution in the general case. SLDE dagger-resolution was introduced by Gallier and Raatz who proved its c
|
|
| 2. |
- Degtyarev, A, et al.
(författare)
-
Equality elimination for the tableau method
- 1996
-
Ingår i: DESIGN AND IMPLEMENTATION OF SYMBOLIC COMPUTATION SYSTEMS. - : SPRINGER-VERLAG BERLIN. - 0302-9743. ; 1128, s. 46-60
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)abstract
- We apply the equality elimination method to semantic tableaux with equality. The resulting logical system is a combination of a goal-directed tableau calculus with a basic superposition calculus. Unlike most other known methods of adding equality to seman
|
|
| 3. |
- Degtyarev, A, et al.
(författare)
-
Simultaneous rigid E-unification is undecidable
- 1996
-
Ingår i: COMPUTER SCIENCE LOGIC. - : SPRINGER-VERLAG BERLIN. - 0302-9743. ; 1092, s. 178-190
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)abstract
- Simultaneous rigid E-unification was introduced in 1987 by Gallier, Raatz and Snyder. It is used in the area of automated reasoning with equality in extension procedures, like the tableau method or the connection method. There were several faulty proofs o
|
|
| 4. |
- Degtyarev, A, et al.
(författare)
-
The decidability of simultaneous rigid E-unification with one variable
- 1998
-
Ingår i: REWRITING TECHNIQUES AND APPLICATIONS. - : SPRINGER-VERLAG BERLIN. - 0302-9743. ; 1379, s. 181-195
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)abstract
- We show that simultaneous rigid E-unification, or SREU for short, is decidable and in fact EXPTIME-complete in the case of one variable. This result implies that the For All*There Exists For All* fragment of intuitionistic logic with equality is decidable
|
|
| 5. |
- Degtyarev, A, et al.
(författare)
-
The undecidability of simultaneous rigid E-unification
- 1996
-
Ingår i: THEORETICAL COMPUTER SCIENCE. - : ELSEVIER SCIENCE BV. - 0304-3975. ; 166:1-2, s. 291-300
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)abstract
- Simultaneous rigid E-unification was introduced in 1987 by Gallier, Raatz and Snyder. It is used in the area of automated reasoning with equality in extension procedures, like the tableau method or the connection method. Many articles in this area assumed
|
|
| 6. |
- Degtyarev, A, et al.
(författare)
-
What you always wanted to know about rigid E-unification
- 1998
-
Ingår i: JOURNAL OF AUTOMATED REASONING. - : KLUWER ACADEMIC PUBL. - 0168-7433. ; 20:1-2, s. 47-80
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)abstract
- This paper solves an open problem posed by a number of researchers: the construction of a complete calculus for matrix-based methods with rigid E-unification. The use of rigid E-unification and simultaneous rigid E-unification for such methods was propose
|
|
| 7. |
- Degtyarev, A, et al.
(författare)
-
What you always wanted to know about rigid E-unification
- 1996
-
Ingår i: LOGICS IN ARTIFICIAL INTELLIGENCE. - : SPRINGER-VERLAG BERLIN. ; 1126, s. 50-69
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)abstract
- This paper solves an open problem posed by a number of researchers: the construction of a complete calculus for matrix-based methods with rigid E-unification. The use of rigid E-unification and simultaneous rigid E-unification for such methods has been pr
|
|
