The Use of Max-Sat for Optimal Choice of Automated Theory Repairs

Marius Urbonas, Alan Bundy, Juan Casanova, Xue Li

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

The ABC system repairs faulty Datalog theories using a combination of abduction, belief revision and conceptual change via reformation. Abduction and Belief Revision add/delete axioms or delete/add preconditions to rules, respectively. Reformation repairs them by changing the language of the faulty theory. Unfortunately, the ABC system overproduces repair suggestions. Our aim is to prune these suggestions to leave only a Pareto front of the optimal ones. We apply an algorithm for solving Max-Sat problems, which we call the Partial Max-Sat algorithm, to form this Pareto front
Original languageEnglish
Title of host publicationArtificial Intelligence XXXVII (SGAI 2020)
EditorsMax Bramer, Richard Ellis
PublisherSpringer, Cham
Pages49-63
Number of pages15
ISBN (Electronic)978-3-030-63799-6
ISBN (Print)978-3-030-63798-9
DOIs
Publication statusPublished - 8 Dec 2020
EventFortieth SGAI International Conference on Artificial Intelligence - A virtual conference, Cambridge, United Kingdom
Duration: 8 Dec 202017 Dec 2020
http://www.bcs-sgai.org/ai2020/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume12498
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349
NameLecture Notes in Artificial Intelligence
PublisherSpringer
Volume12498

Conference

ConferenceFortieth SGAI International Conference on Artificial Intelligence
Abbreviated titleAI-2020
Country/TerritoryUnited Kingdom
CityCambridge
Period8/12/2017/12/20
Internet address

Keywords

  • Faulty logical theory repair
  • Max-Sat
  • Reformation
  • Belief revision
  • Abduction
  • Datalog theories
  • Automated theorem proving

Fingerprint

Dive into the research topics of 'The Use of Max-Sat for Optimal Choice of Automated Theory Repairs'. Together they form a unique fingerprint.

Cite this