🚀 go-pugleaf

Lecture Series ``Collegium Logicum''
Kurt Goedel Society
University of Technology, Vienna, Austria


THEOREM PROVING EVENING
=======================
Monday, June 6, 1994



RICARDO CAFERRA
===============
LIFIA-IMAG Grenoble, France
[caferra@silene.imag.fr]


16:45     Model Building in Theorem Proving
          ---------------------------------

A method for building models in the framework of resolution--paramodulation
is presented.  Given a conjecture, the method looks simultaneously for
refutations  and models. The main idea is to set conditions *both to apply*
inference rules and *to avoid* their application.  The first
conditions correspond to inference rules and the latter to the
so-called  dis-inference rules. These conditions are coded as
*constraints* of the clauses defining a kind of dynamic sorts.

Two versions of the method are presented (both using the same ideas):
the first one for first-order clauses without equality and the second
for equational clauses.  The main theoretical properties are given
as well as comparisons with other existing approaches. In particular
we show how our method can simulate (at least partially) others.  
We emphasize the *unified* approach of our method.
Finally, we present some experiments with the system
implemented in the framework of our Inference Laboratory.



VALERY MIKHAILOV
================
Kazan University, Russia
[mikhailv@univex.kazan.su]


18:00     Theorem Proving in Set Theory
          -----------------------------

A scheme of an interactive method of theorem proving
based on resolution procedures and models constructing is
proposed. The use of this scheme for a particular applied area may
be connected with rather difficult problems. It is necessary to
elaborate a formalization method and a method of constructing an
applied model for given area. After that, in the process of proving a
complicated theorem, one needs to point out only non-trivial
constructions or to choose them from an appropriate knowledge base.
A complete proof or refutation model will be constructed
automatically. A theorem prover and algorithms realizing the scheme
for axiomatic set theory have been elaborated.


------------------------
Kurt-Goedel-Gesellschaft
Technische Universitaet Wien
Institut fuer Computersprachen E185.2
Resselgasse 3/1, A-1040 Wien

Tel: (+43 1) 588 01/4088
Fax: (+43 1) 504 15 89
email: kgs@logic.tuwien.ac.at

Mit Unterstuetzung des
Bundesministeriums fuer Wissenschaft und Forschung