CALL FOR PARTICIPATION

CADE-15 Tutorial on

Clause Normalform Tableaux

Monday, July, 6, 1998

Peter Baumgartner and Ulrich Furbach

University of Koblenz, Germany,

http://www.*-*-*.com/ ~peter/

http://www.*-*-*.com/ ~uli/

[{*filter*}version included below ]

General

-------

Tableaux offer a unifying view to various calculi which are used in

modern high performance theorem provers and logic programming systems;

they are a major deduction paradigm used in the German research

programm "Deduction" and have been shown there as a serious

alternative to resolution-based systems.

Tableaux are furthermore attractive as a framework to compare calculi

which appear different on a first glance. In the tutorial we will

concentrate on this aspect. We will cover top down calculi like

connection calculi and model elimination as well as bottom up

procedures such as Hyper Tableaux and SATCHMO-like procedures. Special

interest is on variants of these calculi which do not use

contrapositives of clauses and hence allow a procedural logic

programming view of clauses.

Objective of the Tutorial

-------------------------

The main issue of this tutorial is to describe the spectrum of clause

normal form tableau based theorem proving, including problem solving

questions and the relation to other calculi. Especially the latter may

help to demonstrate the possibilities of tableau techniques to

describe and to improve proof procedures for first order clause normal

form theorem proving.

For the tutorial, we assume that participants know basics of

first-order theorem proving.

Contents

--------

I From analytic tableaux to clause normal form tableaux.

Sequent Systems and Tableaux for non-clausal logic (in brief).

Unification in Tableaux.

II Goal oriented calculi.

Bibel's connection calculi and its relation to Loveland's model

elimination. Refinements of model elimination and their properties

(regularity, proof procedures, confluence). Proof Procedures based on

the PTTP technique. Relation to other proof procedures like

nearHorn-Prolog or Plaisted's problem reduction formats. Answer

Computing and Logic Programming applications.

III Bottom up computation and model generation.

SATCHMO-like calculi as tableau calculi. Hypertableaux and its

relation to SLO-resolution and Plaisted's Hyper Linking

calculus. Proof search in confluent tableau calculi: Billons

Disconnection calculus, an improved Hypertableau calculus, connection

calculi with rigid variables. Applications for non-monotonic reasoning

and qualitative and diagnostic reasoning.

Registration

------------

Please use the CADE registration form

http://www.*-*-*.com/ ~cade-15/RegoForm....

Deadline for early registration is May, 15.

Further information

-------------------

CADE-15 Web Site -- http://www.*-*-*.com/

TUTORIAL Web Site -- http://www.*-*-*.com/ ~peter/cade-15-tutorial/

Latex call for participation:

\documentstyle{article}

%%%%%% Setting of the various dimensions

\setlength{\textwidth}{17.1cm}

\setlength{\textheight}{27cm}

\setlength{\hoffset}{-3cm}

\setlength{\voffset}{-3.7cm}

%%%%%% definition of the macros: this should not be edited

\newenvironment{Presentation}{\noindent

% For general presentation:

\newline}{~\newline}

\begin{document}

\thispagestyle{empty}

\begin{center}

{\Huge\bf CADE-15}

\\[.6cm]

{\LARGE The 15th International Conference on Automated Deduction}\\[.4cm]

{\Large\it July 5-10, 1998, Lindau, Germany}\\[6mm]

{\LARGE\bf Clause Normalform Tableaux}

\\[.6cm]

{\Large\it July 6}

\\[.6cm]

{\Large\bf Peter Baumgartner and Ulrich Furbach}

\\[.6cm]

{\LARGE Call for Participation}

\end{center}

\begin{Presentation}

% Tutorial presentation: Describe here the general

% purpose of your tutorial and the addressed topics

% adjust \vspace{12cm} according to the size of your description.

%\vspace{12cm}

% This seems to be slightly more convenient:

%\noindent\vbox to 12cm{

% \begin{minipage}{\textwidth}

\paragraph{General.}

Tableaux offer a unifying view to various calculi which are used in

modern high performance theorem provers and logic programming systems;

they are a major deduction paradigm used in the German research

programm ``Deduction'' and have been shown

there as a serious alternative to resolution-based systems.

Tableaux are furthermore attractive as a framework to compare calculi

which appear different on a first glance. In the tutorial we will

concentrate on this aspect. We will cover top down calculi

like connection calculi and model elimination as well as bottom up

procedures such as Hyper Tableaux and SATCHMO-like procedures.

Special interest is on variants of these calculi which do not use

contrapositives of clauses and hence allow a procedural logic

programming view of clauses.

\paragraph{Objective of the Tutorial.}

The main issue of this tutorial is to describe the spectrum of clause

normal form tableau based theorem proving, including problem solving

questions and the relation to other calculi. Especially the latter may

help to demonstrate the possibilities of tableau techniques to

describe and to improve proof procedures for first order clause normal

form theorem proving.

For the tutorial, we assume that participants know basics of

first-order theorem proving.

\paragraph{Contents.} \mbox{}\\

\emph{I\quad From analytic tableaux to clause normal form tableaux.} \\

Sequent Systems and Tableaux for non-clausal logic (in brief).

Unification in Tableaux.\medskip\par

\noindent \emph{II\quad Goal oriented calculi.} \\

Bibel's connection calculi and its relation to

Loveland's model elimination.

Refinements of model elimination and their properties

(regularity, proof procedures, confluence).

Proof Procedures based on the PTTP technique.

Relation to other proof procedures like nearHorn-Prolog or

Plaisted's problem reduction formats.

Answer Computing and Logic Programming applications.

\medskip\par

\noindent \emph{III\quad Bottom up computation and model generation.}\\

SATCHMO-like calculi as tableau calculi.

Hypertableaux and its

relation

to SLO-resolution and Plaisted's Hyper Linking calculus.

Proof search in confluent tableau calculi: Billons

Disconnection calculus,

an improved Hypertableau calculus, connection

calculi with rigid variables.

Applications for non-monotonic reasoning and qualitative and

diagnostic reasoning.

% \end{minipage}

%\vfill}

\end{Presentation}

~~\\[3mm]

\vspace{.3cm}

\begin{center}

\vspace{.5cm}

\fbox{\bf TUTORIAL Web Site --- \tt http://www.*-*-*.com/ ~peter/cade-15-tutorial/}

\vspace{.5cm}

\fbox{\bf CADE-15 Web Site --- \tt http://www.*-*-*.com/ }

\end{center}

\end{document}

--

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Peter Baumgartner Universitaet Koblenz-Landau

Tel: (+49) 261/9119-426 Institut fuer Informatik

Fax: (+49) 261/9119-496 Rheinau 1

WWW: http://www.*-*-*.com/ ~peter/ Germany

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~