# PROOFS AND REFUTATIONS IN NON-CLASSICAL LOGICS (in conjunction with Tableaux 2009) Oslo, Norway, July 6, 2009

A one day workshop on Proofs and Refutations in Non-Classical Logics will be held in July 2009 in conjunction with Tableaux 2009

Hardcopies of the preliminary proceedings will be distributed at the workshop and a Special Issue of a Journal on these topics is expected after the workshop.

## Topics

There has recently been much interest in the design of deduction systems based on the notion of refutation. By refutation we mean a witness of the invalidity of a proposition (formula, sequent, etc.) just as a proof is a witness of the validity of a proposition. There are various ways to design a refutation-based deduction system. We list the following approaches but the workshop is not restricted to them: deduction systems where refutations completely replace proofs as first-class citizens, with a set of rules inductively defining refutation trees; systems combining proof-rules and refutation mechanisms (or criteria) which can occur at various levels of the proof-search process; systems where provability and refutability play dual roles, i.e.,proofs and refutations are both first-class citizens; systems where refutations are understood as mechanisms that build counter-models: for example, semantic information is collected and may converge to a counter-model as the search process evolves.

Such approaches are applicable to a wide range of logics like sub-structural logics including linear or bunched logics and their extensions, intuitionistic or intermediate logics and their extensions, modal or temporal logics, even type theory. The deduction systems can be based on various structures/methods: sequents, tableaux, natural deduction, connections, proof-nets, games, etc.

The aim of the workshop is to provide a forum of discussion between research interested in non-classical logics in the perspective of proof and refutation systems.

Topics of interest, in this context, include but are not restricted to, the following aspects:

• theoretical aspects: new combinations of proofs and refutations, new calculi, completeness, cut-elimination, complexity, semantics, decidability.
• practical aspects: decision procedures, strategies, structures and semantic information (graphs, nets), sharing/duplication avoidance, implementation techniques.
• application aspects: from refutations/counter-models to specifications, counter-models for the end-user, proofs of properties and programs.

## Calls

Call for Papers (.pdf file)

## Submissions

Researchers interested in presenting their works are invited to send an extended abstract (up to 10 pages)} by e-mail submission of a Postscript or PDF file to Didier Galmiche (Didier.Galmiche@loria.fr) by May 15, 2009. Papers will be reviewed by peers, typically members of the programme committee. The cover page should include a return mailing address and, if possible, an electronic mail address and a fax number.

```Didier Galmiche
LORIA UMR 7503 & Universite Henri Poincare
Campus Scientifique, B.P. 239
54506 Vandoeuvre-les-Nancy, France
email: Didier.Galmiche@loria.fr
fax: [+33] 03 83 41 30 79
URL: http://www.loria.fr/~galmiche
```

Program Committee

• R. Dyckhoff (Univ. St Andrews, Scotland)
• C. Fermueller (T.U. Wien, Austria)
• D. Galmiche (LORIA - UHP, France)
• D. Larchey-Wendling (LORIA -CNRS, France)
• F. Pfenning (CMU, Pittsburgh, USA)
• A. Waaler (Univ. Oslo, Norway)

## Important dates:

• 15 May, 2009: submission deadline