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 / Description of output

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
Number of pages15
ISBN (Electronic)978-3-030-63799-6
ISBN (Print)978-3-030-63798-9
Publication statusPublished - 8 Dec 2020
EventFortieth SGAI International Conference on Artificial Intelligence - A virtual conference, Cambridge, United Kingdom
Duration: 8 Dec 202017 Dec 2020

Publication series

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


ConferenceFortieth SGAI International Conference on Artificial Intelligence
Abbreviated titleAI-2020
Country/TerritoryUnited Kingdom
Internet address

Keywords / Materials (for Non-textual outputs)

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


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