View in EDS

A PROOF PROCEDURE FOR TEMPORAL LOGIC PROGRAMMING.

Saved in:
Bibliographic Details
Title: A PROOF PROCEDURE FOR TEMPORAL LOGIC PROGRAMMING.
Authors: Gergatsoulis, Manolis1 manolis@ionio.gr, Nomikos, Christos2 cnomikos@cs.uoi.gr
Source: International Journal of Foundations of Computer Science. Apr2004, Vol. 15 Issue 2, p417-443. 27p.
Subjects: Logic programming, Programming languages, Electronic data processing, Proof theory, Mathematical logic, Automatic theorem proving
Abstract: In this paper, we propose a new resolution proof procedure for the branching-time logic programming language Cactus. The particular strength of the new proof procedure, called CSLD-resolution, is that it can handle, in a more general way, open-ended queries, i.e. goal clauses that include atoms which do not refer to specific moments in time, without the need of enumerating all their canonical instances. We also prove soundness, completeness and independence of the computation rule for CSLD-resolution. The new proof procedure overcomes the limitations of a family of proof procedures for temporal logic programming languages, which were based on the notions of canonical program and goal clauses. Moreover, it applies directly to Chronolog programs and it can be easily extended to apply to multi-dimensional logic programs as well as to Chronolog(MC) programs. [ABSTRACT FROM AUTHOR]
Copyright of International Journal of Foundations of Computer Science is the property of World Scientific Publishing Company and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 12918721
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: A PROOF PROCEDURE FOR TEMPORAL LOGIC PROGRAMMING.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Gergatsoulis%2C+Manolis%22">Gergatsoulis, Manolis</searchLink><relatesTo>1</relatesTo><i> manolis@ionio.gr</i><br /><searchLink fieldCode="AR" term="%22Nomikos%2C+Christos%22">Nomikos, Christos</searchLink><relatesTo>2</relatesTo><i> cnomikos@cs.uoi.gr</i>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22International+Journal+of+Foundations+of+Computer+Science%22">International Journal of Foundations of Computer Science</searchLink>. Apr2004, Vol. 15 Issue 2, p417-443. 27p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Logic+programming%22">Logic programming</searchLink><br /><searchLink fieldCode="DE" term="%22Programming+languages%22">Programming languages</searchLink><br /><searchLink fieldCode="DE" term="%22Electronic+data+processing%22">Electronic data processing</searchLink><br /><searchLink fieldCode="DE" term="%22Proof+theory%22">Proof theory</searchLink><br /><searchLink fieldCode="DE" term="%22Mathematical+logic%22">Mathematical logic</searchLink><br /><searchLink fieldCode="DE" term="%22Automatic+theorem+proving%22">Automatic theorem proving</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: In this paper, we propose a new resolution proof procedure for the branching-time logic programming language Cactus. The particular strength of the new proof procedure, called CSLD-resolution, is that it can handle, in a more general way, open-ended queries, i.e. goal clauses that include atoms which do not refer to specific moments in time, without the need of enumerating all their canonical instances. We also prove soundness, completeness and independence of the computation rule for CSLD-resolution. The new proof procedure overcomes the limitations of a family of proof procedures for temporal logic programming languages, which were based on the notions of canonical program and goal clauses. Moreover, it applies directly to Chronolog programs and it can be easily extended to apply to multi-dimensional logic programs as well as to Chronolog(MC) programs. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of International Journal of Foundations of Computer Science is the property of World Scientific Publishing Company and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=12918721
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1142/S0129054104002509
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 27
        StartPage: 417
    Subjects:
      – SubjectFull: Logic programming
        Type: general
      – SubjectFull: Programming languages
        Type: general
      – SubjectFull: Electronic data processing
        Type: general
      – SubjectFull: Proof theory
        Type: general
      – SubjectFull: Mathematical logic
        Type: general
      – SubjectFull: Automatic theorem proving
        Type: general
    Titles:
      – TitleFull: A PROOF PROCEDURE FOR TEMPORAL LOGIC PROGRAMMING.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Gergatsoulis, Manolis
      – PersonEntity:
          Name:
            NameFull: Nomikos, Christos
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 04
              Text: Apr2004
              Type: published
              Y: 2004
          Identifiers:
            – Type: issn-print
              Value: 01290541
          Numbering:
            – Type: volume
              Value: 15
            – Type: issue
              Value: 2
          Titles:
            – TitleFull: International Journal of Foundations of Computer Science
              Type: main
ResultId 1