Campus Event Calendar
Event Entry
What and Who
PhD Application Talk: Labelled Splitting
Arnaud Fietzke
Talk
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, RG2
MPI Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 29 October 2007
08:00
480 Minutes
E1 4
024
Saarbrücken
Abstract
Saturation-based theorem provers are typically
based on a calculus consisting of inference and
reduction rules that operate on sets of clauses.
While inference rules produce new clauses,
reduction rules allow the removal or simplification
of redundant clauses and are an essential
ingredient for efficient implementations.
The power of reduction rules can be further amplified
by the use of the splitting rule, which is based
on explicit case analysis on variable-disjoint components
of clauses.
In my Master thesis, I give a formalization of splitting
and backtracking for first-order logic using a
labelling scheme that annotates clauses and clause
sets with additional information, and I prove soundness
and completeness results for the corresponding calculus.
The backtracking process as formalized here generalizes
optimizations that are currently being used,
and I present the results of integrating the improved
backtracking into the SPASS theorem prover.
based on a calculus consisting of inference and
reduction rules that operate on sets of clauses.
While inference rules produce new clauses,
reduction rules allow the removal or simplification
of redundant clauses and are an essential
ingredient for efficient implementations.
The power of reduction rules can be further amplified
by the use of the splitting rule, which is based
on explicit case analysis on variable-disjoint components
of clauses.
In my Master thesis, I give a formalization of splitting
and backtracking for first-order logic using a
labelling scheme that annotates clauses and clause
sets with additional information, and I prove soundness
and completeness results for the corresponding calculus.
The backtracking process as formalized here generalizes
optimizations that are currently being used,
and I present the results of integrating the improved
backtracking into the SPASS theorem prover.
Contact
IMPRS-CS
-255
--email hidden
passcode not visible
logged in users only
Tags, Category, Keywords and additional notes
Please note: The talks will take place in random order!
Katja Schönborn, 10/26/2007 14:18
Katja Schönborn, 10/24/2007 13:49
Katja Schönborn, 10/24/2007 13:48 -- Created document.
Katja Schönborn, 10/24/2007 13:49
Katja Schönborn, 10/24/2007 13:48 -- Created document.