liu.seSearch for publications in DiVA
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • 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
Signed Dual Tableaux for Kleene Answer Set Programs
Linköping University, Department of Computer and Information Science, Artificial Intelligence and Integrated Computer Systems. Linköping University, Faculty of Science & Engineering.
Linköping University, Department of Computer and Information Science, Artificial Intelligence and Integrated Computer Systems. Linköping University, Faculty of Science & Engineering.
2018 (English)In: Ewa Orłowska on Relational Methods in Logic and Computer Science / [ed] Golińska-Pilarek J., Zawidzki M., Cham: Springer, 2018, p. 233-252Chapter in book (Refereed)
Abstract [en]

Dual tableaux were introduced by Rasiowa and Sikorski (1960) as a cut free deduction system for classical first-order logic. In the current paper, a sound and complete proof procedure based on dual tableaux is proposed for

R3

which is the standard Kleene logic augmented with a weak negation connective and an implication connective proposed, in another context, by Shepherdson (1989).

R3

is used as a basis for defining Kleene Answer Set Programs (

ASPK

programs). The semantics for

ASPK

programs is based on strongly supported models. Both entailment procedures and model generation procedures for normal and non-normal

ASPK

programs are proposed based on the use of dual tableaux and a model filtering technique. The dual tableau proof procedure extended with a model filtering technique is shown to be sound and complete for

ASPK

programs, both normal and non-normal. Since there is a direct relationship between answer sets for classical ASP programs and

R3

models for

ASPK

programs, it can be shown that the sound and complete dual tableaux proof procedure with filtering for ASPK" role="presentation">ASPKprograms is also sound and complete for classical normal ASP programs. For classical non-normal ASP programs, the proof procedure is only sound, since an alternative semantics for disjunction is used in

ASPK

Place, publisher, year, edition, pages
Cham: Springer, 2018. p. 233-252
Series
Outstanding Contributions to Logic ; 17
Keywords [en]
Signed tableaux, Signed dual tableaux, Answer set programming, Kleene three-valued logic, Strongly supported model
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:liu:diva-153431DOI: 10.1007/978-3-319-97879-6_9ISBN: 9783319978789 (print)ISBN: 9783319978796 (electronic)OAI: oai:DiVA.org:liu-153431DiVA, id: diva2:1270901
Available from: 2018-12-14 Created: 2018-12-14 Last updated: 2019-01-10Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full text

Authority records BETA

Doherty, PatrickSzalas, Andrzej

Search in DiVA

By author/editor
Doherty, PatrickSzalas, Andrzej
By organisation
Artificial Intelligence and Integrated Computer SystemsFaculty of Science & Engineering
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 23 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • 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