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

Marius Urbonas; Alan Bundy; Juan Casanova; Xue Li

doi:10.1007/978-3-030-63799-6_4

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 proceeding › Conference 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 language	English
Title of host publication	Artificial Intelligence XXXVII (SGAI 2020)
Editors	Max Bramer, Richard Ellis
Publisher	Springer
Pages	49-63
Number of pages	15
ISBN (Electronic)	978-3-030-63799-6
ISBN (Print)	978-3-030-63798-9
DOIs	https://doi.org/10.1007/978-3-030-63799-6_4
Publication status	Published - 8 Dec 2020
Event	Fortieth SGAI International Conference on Artificial Intelligence - A virtual conference, Cambridge, United Kingdom Duration: 8 Dec 2020 → 17 Dec 2020 http://www.bcs-sgai.org/ai2020/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	12498
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Name	Lecture Notes in Artificial Intelligence
Publisher	Springer
Volume	12498

Conference

Conference	Fortieth SGAI International Conference on Artificial Intelligence
Abbreviated title	AI-2020
Country/Territory	United Kingdom
City	Cambridge
Period	8/12/20 → 17/12/20
Internet address	http://www.bcs-sgai.org/ai2020/

Keywords / Materials (for Non-textual outputs)

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

Access to Document

10.1007/978-3-030-63799-6_4Licence: All Rights Reserved

AI_2020_Max_SatAccepted author manuscript, 279 KBLicence: Creative Commons: Attribution (CC-BY)
The Use of Max-Sat for Optimal Choice of Automated Theory Repairs (Long Version)Other version, 317 KBLicence: Creative Commons: Attribution (CC-BY)

https://link.springer.com/chapter/10.1007/978-3-030-63799-6_4Licence: All Rights Reserved

The integration and interaction of multiple mathematical Reasoning Processes
Bundy, A., Aspinall, D., Colton, S., Fleuriot, J., Gow, J., Grov, G., Ireland, A., Jackson, P., Mcneill, F., Michaelson, G. & Smaill, A.
EPSRC
1/11/15 → 31/10/19
Project: Research

Cite this

Urbonas, M., Bundy, A., Casanova, J., & Li, X. (2020). The Use of Max-Sat for Optimal Choice of Automated Theory Repairs. In M. Bramer, & R. Ellis (Eds.), Artificial Intelligence XXXVII (SGAI 2020) (pp. 49-63). (Lecture Notes in Computer Science; Vol. 12498), (Lecture Notes in Artificial Intelligence ; Vol. 12498). Springer. https://doi.org/10.1007/978-3-030-63799-6_4

@inproceedings{0fd42d933f5645a1a6297bd646e21d68,

title = "The Use of Max-Sat for Optimal Choice of Automated Theory Repairs",

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",

keywords = "Faulty logical theory repair, Max-Sat, Reformation, Belief revision, Abduction, Datalog theories, Automated theorem proving",

author = "Marius Urbonas and Alan Bundy and Juan Casanova and Xue Li",

year = "2020",

month = dec,

day = "8",

doi = "10.1007/978-3-030-63799-6_4",

language = "English",

isbn = "978-3-030-63798-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "49--63",

editor = "Max Bramer and Richard Ellis",

booktitle = "Artificial Intelligence XXXVII (SGAI 2020)",

note = "Fortieth SGAI International Conference on Artificial Intelligence, AI-2020 ; Conference date: 08-12-2020 Through 17-12-2020",

url = "http://www.bcs-sgai.org/ai2020/",

}

Urbonas, M, Bundy, A, Casanova, J & Li, X 2020, The Use of Max-Sat for Optimal Choice of Automated Theory Repairs. in M Bramer & R Ellis (eds), Artificial Intelligence XXXVII (SGAI 2020). Lecture Notes in Computer Science, vol. 12498, Lecture Notes in Artificial Intelligence , vol. 12498, Springer, pp. 49-63, Fortieth SGAI International Conference on Artificial Intelligence, Cambridge, United Kingdom, 8/12/20. https://doi.org/10.1007/978-3-030-63799-6_4

The Use of Max-Sat for Optimal Choice of Automated Theory Repairs. / Urbonas, Marius; Bundy, Alan; Casanova, Juan et al.
Artificial Intelligence XXXVII (SGAI 2020). ed. / Max Bramer; Richard Ellis. Springer, 2020. p. 49-63 (Lecture Notes in Computer Science; Vol. 12498), (Lecture Notes in Artificial Intelligence ; Vol. 12498).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

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

AU - Urbonas, Marius

AU - Bundy, Alan

AU - Casanova, Juan

AU - Li, Xue

PY - 2020/12/8

Y1 - 2020/12/8

N2 - 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

AB - 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

KW - Faulty logical theory repair

KW - Max-Sat

KW - Reformation

KW - Belief revision

KW - Abduction

KW - Datalog theories

KW - Automated theorem proving

U2 - 10.1007/978-3-030-63799-6_4

DO - 10.1007/978-3-030-63799-6_4

M3 - Conference contribution

SN - 978-3-030-63798-9

T3 - Lecture Notes in Computer Science

SP - 49

EP - 63

BT - Artificial Intelligence XXXVII (SGAI 2020)

A2 - Bramer, Max

A2 - Ellis, Richard

PB - Springer

T2 - Fortieth SGAI International Conference on Artificial Intelligence

Y2 - 8 December 2020 through 17 December 2020

ER -

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

Abstract / Description of output

Publication series

Conference

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Projects

The integration and interaction of multiple mathematical Reasoning Processes

Cite this