Campus Event Calendar
Event Entry
What and Who
Prime Implicates Generation in Equational Logic
Sophie Tourret
Japanese National Institute of Informatics
Talk
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI
Public Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 9 January 2017
14:00
60 Minutes
E1 5
029
Saarbrücken
Abstract
In this presentation, I will talk about the work I did during
my PhD thesis on the generation of prime implicates in equational
logic, i.e., the most general consequences of formulae containing
equations and disequations between first-order terms. I will
present the main result of this research, which is an algorithm
for generating prime implicates that relies on an extension of
the standard Superposition Calculus with rules that allow attaching
hypotheses to clauses as constraints to perform additional inferences.
The hypotheses that lead to a refutation represent implicates of
the original set of clauses. The set of prime implicates of a clausal
set can thus be obtained by saturation of this set up to redundancy.
I will also introduce the data structures and algorithms that were
devised to represent and manipulate sets of constrained clauses in
an efficient and concise way and a practical experimentation that
show the relevance of this method in comparison to existing
approaches for propositional and first-order logic.
my PhD thesis on the generation of prime implicates in equational
logic, i.e., the most general consequences of formulae containing
equations and disequations between first-order terms. I will
present the main result of this research, which is an algorithm
for generating prime implicates that relies on an extension of
the standard Superposition Calculus with rules that allow attaching
hypotheses to clauses as constraints to perform additional inferences.
The hypotheses that lead to a refutation represent implicates of
the original set of clauses. The set of prime implicates of a clausal
set can thus be obtained by saturation of this set up to redundancy.
I will also introduce the data structures and algorithms that were
devised to represent and manipulate sets of constrained clauses in
an efficient and concise way and a practical experimentation that
show the relevance of this method in comparison to existing
approaches for propositional and first-order logic.
Contact
Jennifer Müller
2900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 01/06/2017 14:47 -- Created document.