No Cover Image

Journal article 984 views

Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution

Matthew Gwynne, Oliver Kullmann Orcid Logo

Journal of Automated Reasoning, Volume: 52, Issue: 1, Pages: 31 - 65

Swansea University Author: Oliver Kullmann Orcid Logo

Full text not available from this repository: check for access using links below.

Check full text

DOI (Published version): 10.1007/s10817-013-9275-8

Abstract

The class SLUR has been introduced in 1995 as an umbrella class for fast SAT solving, while the class UC has been introduced in 1994 for the purpose of knowledge compilation. We now show that SLUR = UC holds, and this in a strongly generalised context, embedding these classes into a rich theory. Fun...

Full description

Published in: Journal of Automated Reasoning
ISSN: 0168-7433 1573-0670
Published: 2014
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa13746
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2013-07-23T12:10:50Z
last_indexed 2019-06-05T09:30:44Z
id cronfa13746
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2019-06-04T14:20:42.5387475</datestamp><bib-version>v2</bib-version><id>13746</id><entry>2012-12-17</entry><title>Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution</title><swanseaauthors><author><sid>2b410f26f9324d6b06c2b98f67362d05</sid><ORCID>0000-0003-3021-0095</ORCID><firstname>Oliver</firstname><surname>Kullmann</surname><name>Oliver Kullmann</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2012-12-17</date><deptcode>SCS</deptcode><abstract>The class SLUR has been introduced in 1995 as an umbrella class for fast SAT solving, while the class UC has been introduced in 1994 for the purpose of knowledge compilation. We now show that SLUR = UC holds, and this in a strongly generalised context, embedding these classes into a rich theory. Fundamental is the notion of "hardness", which is explored here systematically.</abstract><type>Journal Article</type><journal>Journal of Automated Reasoning</journal><volume>52</volume><journalNumber>1</journalNumber><paginationStart>31</paginationStart><paginationEnd>65</paginationEnd><publisher/><issnPrint>0168-7433</issnPrint><issnElectronic>1573-0670</issnElectronic><keywords/><publishedDay>31</publishedDay><publishedMonth>1</publishedMonth><publishedYear>2014</publishedYear><publishedDate>2014-01-31</publishedDate><doi>10.1007/s10817-013-9275-8</doi><url>http://www.cs.swan.ac.uk/~csoliver/papers.html#SLUR2013</url><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2019-06-04T14:20:42.5387475</lastEdited><Created>2012-12-17T22:02:07.2000103</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Matthew</firstname><surname>Gwynne</surname><order>1</order></author><author><firstname>Oliver</firstname><surname>Kullmann</surname><orcid>0000-0003-3021-0095</orcid><order>2</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2019-06-04T14:20:42.5387475 v2 13746 2012-12-17 Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution 2b410f26f9324d6b06c2b98f67362d05 0000-0003-3021-0095 Oliver Kullmann Oliver Kullmann true false 2012-12-17 SCS The class SLUR has been introduced in 1995 as an umbrella class for fast SAT solving, while the class UC has been introduced in 1994 for the purpose of knowledge compilation. We now show that SLUR = UC holds, and this in a strongly generalised context, embedding these classes into a rich theory. Fundamental is the notion of "hardness", which is explored here systematically. Journal Article Journal of Automated Reasoning 52 1 31 65 0168-7433 1573-0670 31 1 2014 2014-01-31 10.1007/s10817-013-9275-8 http://www.cs.swan.ac.uk/~csoliver/papers.html#SLUR2013 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2019-06-04T14:20:42.5387475 2012-12-17T22:02:07.2000103 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Matthew Gwynne 1 Oliver Kullmann 0000-0003-3021-0095 2
title Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution
spellingShingle Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution
Oliver Kullmann
title_short Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution
title_full Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution
title_fullStr Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution
title_full_unstemmed Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution
title_sort Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution
author_id_str_mv 2b410f26f9324d6b06c2b98f67362d05
author_id_fullname_str_mv 2b410f26f9324d6b06c2b98f67362d05_***_Oliver Kullmann
author Oliver Kullmann
author2 Matthew Gwynne
Oliver Kullmann
format Journal article
container_title Journal of Automated Reasoning
container_volume 52
container_issue 1
container_start_page 31
publishDate 2014
institution Swansea University
issn 0168-7433
1573-0670
doi_str_mv 10.1007/s10817-013-9275-8
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
url http://www.cs.swan.ac.uk/~csoliver/papers.html#SLUR2013
document_store_str 0
active_str 0
description The class SLUR has been introduced in 1995 as an umbrella class for fast SAT solving, while the class UC has been introduced in 1994 for the purpose of knowledge compilation. We now show that SLUR = UC holds, and this in a strongly generalised context, embedding these classes into a rich theory. Fundamental is the notion of "hardness", which is explored here systematically.
published_date 2014-01-31T03:15:43Z
_version_ 1763750280616214528
score 11.014537

Similar Items