Post has attachment
Xmas Experiment: Isabelle Mini Clone in Prolog

Just as a little xmas experiment an isabelle clone. There is no guarantee that I managed to get everything right. But I have followed the idea of a degenerate pure type system. Can this be also done?

A little trick helps here. We will introduce a new constant => and see to it that it reflects - > and that it is typable correctly. So we first define this constant as follows:

:- op(1050, xfy, =>).

:- axiom (=>)::prop > prop > prop.
: axiom p:prop.
: axiom q:prop.

?- type p=>q.

How we reflect => logically depends on the calculus we want to implement. The -> can be used to realize the rules of the calculus and to logically produce =>.

Home Work: Extend the logic by quantifiers, extend the type checker by eta and beta conversion, extend the type checker by higher order unification,  etc.. etc..

Alternate Home Work: Try something else than eta
and beta conversion, try something else than higher
order unification, etc.. etc..

Source Code: Debruijn Indexes

Source Code: Natural Deduction

Source Code: Sequent Calculus

  APPA - ∀X.Xπ - All about Proofs, Proofs for All
          ++ Tutorials about Proofs ++
         July 18, 2014, Vienna, Austria

           --- call for participation ---

Register now at, selecting "APPA" on workshop block 2. 
Early-registered participants will receive a book with the invited papers. 
Early registration goes until 8th of June.


Many of us, logicians, devote our work to the improvement of proofs, proof systems, proof formats, interactive proof script languages, proof search methods... But what makes a proof (system|format|search-method|...) better than another? Logicians from different communities will give radically different answers to this question! The principles behind their answers may be unknown to outsiders; they may even sound obscure, ungrounded or in apparent contradiction to the principles of other communities.

The Vienna Summer of Logic presents a unique opportunity to promote a conversation between all communities on questions related to proofs. ∀X.XΠ will promote a fruitful knowledge exchange by organizing short tutorials given by prominent speakers from various communities. These tutorials shall be accessible to young researchers and of interest to experienced researchers from other communities as well. 

Tutorial Topics and Speakers

- SAT-Solvers: 
+ Marijn Heule (University of Texas at Austin, USA)

- SMT-Solvers:  
+ Clark Barrett (New York University, USA)
+ Pascal Fontaine (LORIA Nancy, France)
+ Leonardo de Moura (Microsoft Research, USA)

- First-order Automated Theorem Provers: 
+ Stephan Schulz (Munich University of Technology, Germany)

- Higher-order Automated Theorem Provers: 
+ Christoph Benzmüller (Freie Universität Berlin, Germany)

- Interactive Theorem Provers: 
+ Makarius Wenzel (LRI, Université Paris Sud, France)

- Calculus of Inductive Constructions: 
+ Christine Paulin-Mohring (LRI & INRIA Saclay, France)

- Deduction Modulo: 
+ Gilles Dowek (INRIA Paris, France)

- Deep Inference: 
+ Alessio Guglielmi (University of Bath, England)

- Foundational Proof Certificates: 
+ Dale Miller (École Polytechnique, Paris, France)

- Program Verification (B Method): 
+ Jean-Raymond Abrial (ETH Zürich, Switzerland)

- Security:
+ Gilles Barthe (IMDEA Software Institute, Madrid, Spain)

- Mathematical Proof Analysis:
+ Alexander Leitsch (Vienna University of Technology, Austria)


- David Delahaye (Cedric/Cnam/Inria, Paris)
- Bruno Woltzenlogel Paleo (Vienna University of Technology)

For more information, visit:

Post has shared content

Post has shared content

Post has shared content

Google Summer of Code Opportunity on a Project related to Proof Theory

The computer science and engineering group of the Vienna University of Technology has been accepted as a mentoring organization for the 3rd consecutive year in Google's Summer of Code program (, and Skeptik ( is one of its projects.

Skeptik is a tool for checking, compressing and improving formal proofs generated by automated deduction tools, currently focusing on propositional resolution proofs generated by Sat- and SMT-solvers. It implements various recent proof compression algorithms, such as RecyclePivots, RecyclePivotsWithIntersection, Split, Reduce&Reconstruct, LowerUnits, LowerUnivalents, as well as combinations and variants of these algorithms.

Students interested in applying for a Google Summer of Code grant (US$ 5000) to work from 17th of June to 23rd of September on the development of new proof compression algorithms within Skeptik should follow the instructions in this wiki-page:

The DEADLINE for student applications is 3rd of May 2013.

Before preparing their applications, students are encouraged to contact us (preferably by sending a message to our mailinglist ( with "[Skeptik]" in the subject).

Post has attachment

Post has shared content

The Centre for Logic and Philosophy of Science of Ghent University was founded in 1993. On occasion of its 20th anniversary the Centre organises an international Conference on Logic and Philosophy of Science (CLPS13) on the themes that are central to its research:

- Logical analysis of scientific reasoning processes
- Methodological and epistemological analysis of scientific reasoning processes

Conference dates: 16-18 September 2013

Keynote talks will be given by Diderik Batens (the founder of the Centre), three logicians (Natacha Alechina, Graham Priest and Stephen Read) and three philosophers of science (Hanne Andersen, Hasok Chang, and Jim Woodward).

We will also schedule parallel sessions with contributed papers and special symposia with a limited number of papers. I organise a symposium (#4) on


The proof-theoretical understanding of logical relations and properties has received in the last 40 years a significantly new impact from the intuition underlying the so-called Curry-Howard Isomorphism: the contextual validity of a proof is equivalent to the executability of a program in a network. Given the large impact of this identity on theoretical aspects of logic and their applications, bridging formal properties of proofs with computational aspects of programs is of huge importance. Besides the purely syntactical relation between (proof-)validity and (program-) correctness, proof theories for modal, temporal, dynamic logics can be used to verify software and hardware specification in a decidable way. In the debate between denotational and procedural semantics of programming languages a similar paradigm change is at stake where the standard approach to truth is replaced by provability of type preservation and termination of procedures.

Proofs, programs, procedures represent the foundational elements in this novel understanding of traditional logical problems. In this session we will explore formal and epistemic issues that are relevant to proof-theoretical and type-theoretical systems, program logics and procedural semantics. Topics of interest include but are not restricted to:

- proof-theories and type-theories for multi-agent systems, distributed and parallel computing
- formal and meta-theoretical issues in modal, temporal, concurrent systems
- applications of proof-theoretical and type-theoretical models to issues of trust, security, reliability, functioning and malfunctioning
- type-checking, proof-checking and automatization
- procedural semantics for epistemic purposes

If you want to present a paper at this symposium, please upload an abstract in PDF format (between 500 and 1000 words) to: before 1 April 2013.

You will be asked to choose between one of the following submission categories:

- Logical analysis of scientific reasoning processes

- Methodological and epistemological analysis of scientific reasoning processes

- Symposium submission

Select the last option and mention the symposium number in the title of your abstract.

If you do not have an EasyChair account you can create one here:

Unfortunately, we cannot offer any financial support for symposium speakers. Neither can we waive the registration fee.

All abstracts for symposia will be refereed by the organisers and other members of the programme committee. Notification of acceptance will be given by 15 May 2013.

All further information (e.g. accommodation, registration, maps) can be found at the conference website:

The programme will be available on the website by 1 July 2013.

Post has attachment
Second Conference on Proof-Theoretic Semantics

           8-10 March 2013 in Tübingen, Germany

Call for contributed talks

For information on the topic of this conference see .

Invited Speakers are:

- Sergei Artemov
- Kosta Došen
- Roy Dyckhoff
- Lars Hallnäs
- Wilfrid Hodges
- Reinhard Kahle
- Dag Prawitz
- Giovanni Sambin
- Göran Sundholm
- William Tait
- Johan van Benthem
- Jan von Plato
- Heinrich Wansing

There will be a few slots for contributed talks (30 min). If you are 
interested in contributing a talk, please send an abstract to Thomas Piecha 
( by 31 January 2013. We would notify you 
by 10 February of whether we can accept it or not.

Participants who would like to participate without giving a talk are also 
welcome. In that case please send an email to Thomas Piecha by 10 February.
Wait while more posts are being loaded