Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

New for: D1, D2, D3, D4, D5
<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:SGGS: Model-Based First-Order Theorem Proving
Speaker:Maria Paola Bonacina
coming from:Università degli Studi di Verona
Speakers Bio:
Event Type:Talk
Visibility:D1, D2, D3, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:Public Audience
Date, Time and Location
Date:Thursday, 5 June 2014
Duration:60 Minutes
Please note: New Building!
Building:E1 5
Please note: New Room!
SGGS, for Semantically-Guided Goal-Sensitive theorem proving,

is a new inference system for first-order logic. It was inspired
by the idea of generalizing the model-based style of the
Davis-Putnam-Logemann-Loveland (DPLL) procedure, which is a key
feature of SAT solvers, SMT solvers, and model-constructing
decision procedures for specific theories. Model-based reasoning
in first-order logic is challenging: SGGS uses a given interpretation
for semantic guidance; avoids backtracking, because it is proof
confluent; is refutationally complete; and it is goal-sensitive,
if the initial interpretation is properly chosen. In terms of
operations, SGGS combines instance generation, resolution, and
constraints, in a model-centric approach: it uses sequences of
constrained clauses to represent models, instance generation to
extend the model, resolution and other inferences to repair it.
This talk advertises SGGS presenting the main ideas that make its
seemingly rare combination of properties possible.

(Joint work with David A. Plaisted)

Name(s):Jennifer Müller
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:YesTo Location:Kaiserslautern
To Building:G26To Room:112
Meeting ID:
Tags, Category, Keywords and additional notes
Attachments, File(s):
  • Jennifer Müller, 06/05/2014 11:27 AM
  • Jennifer Müller, 05/28/2014 11:07 AM -- Created document.