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
  • 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
An Entailment Procedure 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. (UASTECH – Teknologier för autonoma obemannade flygande farkoster, KPLAB - Laboratoriet för kunskapsbearbetning, KPLAB)
Linköping University, Department of Computer and Information Science, Artificial Intelligence and Integrated Computer Systems. Linköping University, Faculty of Science & Engineering. (KPLAB - Laboratoriet för kunskapsbearbetning, KPLAB)
2016 (English)In: Multi-disciplinary Trends in Artificial Intelligence. MIWAI 2016. / [ed] Sombattheera C., Stolzenburg F., Lin F., Nayak A., Springer, 2016, Vol. 10053, 24-37 p.Conference paper, (Refereed)
Abstract [en]

Classical Answer Set Programming is a widely known knowledge representation framework based on the logic programming paradigm that has been extensively studied in the past decades. Semantic theories for classical answer sets are implicitly three-valued in nature, yet with few exceptions, computing classical answer sets is based on translations into classical logic and the use of SAT solving techniques. In this paper, we introduce a variation of Kleene three-valued logic with strong connectives, R3" role="presentation">R3, and then provide a sound and complete proof procedure for R3" role="presentation">R3 based on the use of signed tableaux. We then define a restriction on the syntax of R3" role="presentation">R3 to characterize Kleene ASPs. Strongly-supported models, which are a subset of R3" role="presentation">R3 models are then defined to characterize the semantics of Kleene ASPs. A filtering technique on tableaux for R3" role="presentation">R3 is then introduced which provides a sound and complete tableau-based proof technique for Kleene ASPs. We then show a translation and semantic correspondence between Classical ASPs and Kleene ASPs, where answer sets for normal classical ASPs are equivalent to strongly-supported models. This implies that the proof technique introduced can be used for classical normal ASPs as well as Kleene ASPs. The relation between non-normal classical and Kleene ASPs is also considered.

Place, publisher, year, edition, pages
Springer, 2016. Vol. 10053, 24-37 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 10053
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:liu:diva-134767DOI: 10.1007/978-3-319-49397-8_3ISI: 000389332100003ISBN: 978-3-319-49396-1 (print)ISBN: 978-3-319-49397-8 (electronic)OAI: oai:DiVA.org:liu-134767DiVA: diva2:1076960
Conference
Multi-disciplinary Trends in Artificial Intelligence. MIWAI 2016.
Projects
CADICSELLIITCUASSymbiCloudNFFP6
Available from: 2017-02-24 Created: 2017-02-24 Last updated: 2017-03-17

Open Access in DiVA

No full text

Other links

Publisher's full text

Search in DiVA

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

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 18 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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