The merits of compositional abstraction: A case study in propositional logic
File(s)
Accepted version
Author(s)
Huth, Michael
Type
Chapter
Abstract
We revisit a well-established and old topic in computational logic: algorithms – such as the one by Quine-McCluskey – that convert a formula of propositional logic into a semantically equivalent disjunctive normal form whose clauses are all prime implicants of that formula. This exercise in education is meant to honor Bernhard Steffen, who made important contributions in formal verification and its use of compositional abstraction, and who is a role model in transferring research insights into teaching addressed at students with varying skill levels. The algorithm we propose here is indeed compositional and can teach students about the value of compositional abstractions – making use of simple lattice-theoretic and semantic concepts.
Date Issued
2019-06-26
Citation
Lecture Notes in Computer Science, 2019, pp.297-309
ISBN
9783030223472
Publisher
Springer International Publishing
Start Page
297
End Page
309
Journal / Book Title
Lecture Notes in Computer Science
Copyright Statement
© Springer Nature Switzerland AG 2019.
Identifier
https://link.springer.com/chapter/10.1007%2F978-3-030-22348-9_18
Subjects
Artificial Intelligence & Image Processing
Publication Status
Published
Date Publish Online
2019-06-26