| 1. |
|
|
| 2. |
- Kreuger, Per
(författare)
-
A-sufficient substitutions in mixed contexts
- 1994. - 1
-
Ingår i: Proceedings of the Workshop Proof-Theoretic Extensions of Logic Programming at the International Conference on Logic Programming, Springer LNAI Extensions of Logic Programming at the International Conference on Logic Programming. ; , s. 38-43
-
Konferensbidrag (refereegranskat)abstract
- In proof-systems based on calculi of Partial Inductive Definitions (PID), the notion of an A-sufficient substitution is of central importance. Applying an A-sufficient substitution to an atom before computing its definiens is necessary for the rule of definitional reflection to be sound. So far computation of A-sufficient substitutions have been restricted to the case where all variables in a query (sequent to be proved) are existentially quantified, i.e. logical variables in the sense of Prolog. From a proof theoretic point of view this kind of variable can be regarded as metavariables i.e. place-holders for as yet unknown terms. In a finitary calculus of PID's these eigenvariables have to be bound by the rule of definitional reflection in order to preserve soundness (with respect to an underlying infinitary system of PID's). This property makes these calculi different from most (if not all) calculi based on more traditional logics. This note explores some computational issues in connectin with such caluculi.
|
|
| 3. |
|
|
| 4. |
- Kreuger, Per
(författare)
-
Axioms in Definitional Calculi
- 1993. - 1
-
Ingår i: Extensions of Logic Programming ELP'93: Proceedings Proceedings of the fourth international workshop on extensions of logic programming, Springer LNAI of the fourth international workshop on extensions of logic programming. - : Springer Verlag. ; , s. 196-205
-
Konferensbidrag (refereegranskat)abstract
- This paper introduces a restricted form of the axiom rule in calculi of Partial Inductive Definitions (PID). The paper argues that in calculi of PIDs the distinction between atomic and non-atomic formulae is not asclear as in traditional sequent calculi. Therefore the common restriction of the axiom rule to the atomic case is not adequate for this type of calculi.A novel proviso for the axiom rule and corresponding provisos for the left and right definition rules are introduced with an accompanying discussion and suggestions for possible applications in the domain of declarative specification of operational behaviour of logic programs.
|
|
| 5. |
- Kreuger, Per
(författare)
-
GCLA II. A definitional approach to control
- 1992. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- This paper describes the logic programming language GCLA II, its operational semantics and parts of its theortical foundations. GCLA II is a generalization of the language GCLA (Generalized Horn Clause Language) argumented by a method to guide and constrain proof search. The method is based on specification of strategies in a meta language that is a sub language of GCLA itself. A GCLA II program is partioned into two distinct parts. One is used to express the declarative content of the program, while the other is used to define the possible inference made from this declarative knowledge. Altough the intended use of the declarative part and the procedural parts are quite different, they can both be described in the formalism of partial inductive definitions. Thus we preserve a declarative reading of the program as a whole. In particular, given certain sythactic constraints on the program, the heuristics associated with proof search does not affect the declarative reading of the declarative part of the program at all. Several experiments intepreters and a compiler from GCLA II to Prolog have been implemented.
|
|
| 6. |
|
|
