# Plan du site

## Articles

• Peut-on avoir raison tout seul ?

Pour Cyrille Imbert
Il s’agit de répondre ici au problème philosophique que pose la question « peut-on avoir raison tout seul ? ». Pour éviter de répéter cette formulation, on la désignera à partir de maintenant par l’expression plus concise « question S ». Comme on va le voir, la question S illustre au (...)

## Automatisation des preuves

• Natural Deduction Prover

, par

The following prover provides proofs in natural deduction with Fitch style for any propositional formula that is valid in classical logic, and counter-models for any propositional formula that is invalid in classical logic.
Remarks : Supposing that A is a formula taken as input to the above (...)

• Intuitionistic Prover via S4

, par

It is well known that once a propositional formula A is translated into a modal formula B via Gödel translation, A is intuitionistically valid if and only if B is valid in S4. If A is intuitionistically valid, then the prover provides a proof that B is valid in S4. Si A is not (...)

• Sequent Prover (seqprover)

, par

This small program seqprover.pl (written in SICStus Prolog and running into this website thanks to SWI-Prolog) searches a cut-free proof of the given sequent of first-order logic. Of course, the proof search of first-order logic is undecidable. Therefore, this program limits the number of (...)

• A Linear Logic Prover

, par

This small program searches a cut-free proof of the given two-sided sequent of first-order linear logic. Of course, the proof search of linear logic is undecidable. Therefore, this program limits the number of contraction rules for each path of the proof at most three (this threshold value can (...)

• G4 Prover

This prover is a fork that I developed from seqprover.pl that is Naoyuki Tamura’s prover for sequent calculus CL-X. I am a lot indebted to Naoyuki Tamura’s work, because I needed to change almost only the logical rules of his program to succeed in writing this prover that provides proof in (...)

• The Tree Proof Generator by Wolfgang Schwarz

Enter a formula of standard propositional, predicate, or modal logic. The page will try to find either a countermodel or a tree proof (a.k.a. semantic tableau).

## [Educasup] FAQ

• How to register and communicate on this mailing list ?

? Why educasup.philo@ml.free.fr ?
The goal of this mailing list is to inform you about philosophical education (in France, in Europe and in the world).
? Who can subscribe to this list ?
All those who are concerned with philosophy teaching are welcome on the list.
? Who can communicate on (...)

• Comment s’inscrire et communiquer sur la liste educasup.philo ?

? Quelle est la fonction de cette liste de diffusion ?
Cette liste est une liste d’information au sujet de tout ce qui concerne l’enseignement philosophique (en France, en Europe et dans le monde).
? Qui peut s’inscrire sur cette liste de diffusion ?
Tous ceux qui sont concernés par (...)