CADE-15 Tutorial 'Clause Normalform Tableaux' 
Author Message
 CADE-15 Tutorial 'Clause Normalform Tableaux'

                        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
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~



Sat, 07 Oct 2000 03:00:00 GMT  
 
 [ 1 post ] 

 Relevant Pages 

1. Reminder: CADE-15 WS 'Problem Solving...'

2. CADE 15 Workshop 'Problem-solving Methodologies...'

3. Call for Participation: CADE-18 / TABLEAUX 2002

4. Problem with 'VALID' clause

5. passage d'un tableau de cluster a une DLL

6. A Question about 'creation' Clauses

7. Help on 'Value' clause

8. 'Static'_simple_expression in component clause?!?

9. Help on 'Value' clause

10. ISOTAS '96 (Mar. 11 - 15) announcement (updated)

11. FroCoS'2000: EXTENDED DEADLINE (OCTOBER 15, 1999)

12. ISOTAS '96 (Mar. 11 - 15) announcement (updated)

 

 
Powered by phpBB® Forum Software