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

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

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Leo-III - Paramodulation-Based Reasoning in HOL
Speaker:Alexander Steen
coming from:FU Berlin
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:AG Audience
Language:English
Date, Time and Location
Date:Friday, 16 September 2016
Time:11:00
Duration:60 Minutes
Location:Saarbrücken
Building:E1 5
Room:630
Abstract
In the DFG funded Leo-III project, an agent-based automated

deduction system for classical higher-order logic (HOL) is
developed. It aims at exploiting massive parallelism at
various levels in the reasoning process by employing independent
agents that are scheduled as optimization procedure using
combinatorical auction games. In its current state, Leo-III is
based on a paramodulation calculus for typed lambda-terms,
augmented with ordering constraints and special means of
extensionality treatment. HOL terms are represented as locally
nameless spine terms, together with perfect term sharing and
explicit substitutions. A key aspect of Leo's reasoning approach
is the cooperation with external specialist provers (most
prominently, but not limited to, first-order provers). In the talk,
we will survey the current state of the Leo-III prover and sketch
ongoing experiments and developments.

Contact
Name(s):Jennifer Müller
Phone:2900
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Note:
Attachments, File(s):

Created by:Jennifer Müller/MPI-INF, 09/14/2016 11:30 AMLast modified by:Uwe Brahm/MPII/DE, 11/24/2016 04:13 PM
  • Jennifer Müller, 09/14/2016 11:32 AM -- Created document.