Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
A-sufficient substitutions in mixed contexts
RISE, Swedish ICT, SICS, Decisions, Networks and Analytics lab.ORCID iD: 0000-0002-9331-0352
1994 (English)In: 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, 1994, 1, Vol. 596, 6 p.38-43 p.Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
1994, 1. Vol. 596, 6 p.38-43 p.
Series
Lecture Notes in Artificial Intelligence
Keyword [en]
Partial Inductive definitions, definiens computation, meta variables
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:ri:diva-21195OAI: oai:DiVA.org:ri-21195DiVA: diva2:1041229
Conference
Workshop Proof-Theoretic Extensions of Logic Programming at the International Conference on Logic Programming
Note

LNAI, Springer

Available from: 2016-10-31 Created: 2016-10-31 Last updated: 2017-10-12Bibliographically approved

Open Access in DiVA

fulltext(102 kB)1 downloads
File information
File name FULLTEXT01.psFile size 102 kBChecksum SHA-512
774c5ea7f61510a0b693c2821cca7c29f4f3ade1413bc3d35d724d11b6d55642fb4e3e869431bfd6950d690f1c8c52d2cedfa1cd9f5f3ebb19a399bf4a26610a
Type fulltextMimetype application/postscript

Search in DiVA

By author/editor
Kreuger, Per
By organisation
Decisions, Networks and Analytics lab
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 1 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf