Abstract:
The motivation for development of relational proof systems comes from
two sources. First, there is an opinion in the theorem proving
community that it is more sensible to implement one generic logic
within which many other logics can be expressed than to continually
reimplement logics from scratch. Second, recently one can observe a
tendency to change the role of specific (non-logical) axioms in
deduction processes. Namely, there are attempts to define deduction
rules that represent the same information as specific axioms, and when
this is possible, to replace those axioms by their respective rules
in
deduction systems. In this way, instead of proving that a formula is
a
consequence of the axioms, one can use the enlarged set of rules to
prove the formula itself. A relational logic can play the role
of a
generic theory for which the axioms may be replaced by the deduction
rules. We present a general method of developing proof systems for
relational logics. We discuss principles of the construction of
deduction rules and correspondences reflecting relationships between
semantics of relational logics and the rules of the respective proof
systems. We illustrate the method with examples from the field of
spatial reasoniing. The content of the talk is based on joint
work
with Ivo Düntsch and Wendy MacCaull.
References
Düntsch, I. and Orlowska, E. (2000) A proof system for contact
relation algebras. Journal of Philosophical Logic 29, 241-262.
Konikowska, B. and Orlowska, E. (2001) A relational formalisation of
a
generic many-valued modal logic. In: E. Orlowska and A. Szalas (eds)
Relational Methods for Computer Science Applications, Springer -
Physica Verlag, Heidelberg, 183-202.
MacCaull, W. (1997) Relational proof theory for linear and other
substructural logics. Logic Journal of the Interest Group of Pure and
Applied Logic 5, 673-697.
MacCaull, W. and Or?owska, E. (2001) Correspondence results for
relational proof systems with application to the Lambek
calculus. Studia Logica, to appear.