_____ __ ___
/ ____| \ \ / / |
| | ___ _ __ _ __ \ V /| | ___ __ _
| | / _ \| '_ \| '_ \ > < | | / _ \ / _` |
| |___| (_) | | | | | | |/ . \| |___| (_) | (_| |
\_____\___/|_| |_|_| |_/_/ \_\______\___/ \__, |
__/ |
|___/
Université : Université de Lorraine (Nancy) — Département Informatique
Module : M1 S8 — Preuves & déductions automatisées
Auteurs : PiTuring & Metheor31Game
Encadrant : Didier Galmiche
Année universitaire : 2025-2026
Licence : MIT — voir LICENSE
Ce dépôt contient une implémentation pédagogique en Prolog de la méthode des connexions, un calcul de démonstration automatique de théorèmes développé par Wolfgang Bibel (1974) et étendu aux logiques non classiques par Lincoln Wallen (1990).
A poursuivre.
A DEFINIR
A DEFINIR
A DEFINIR
A DEFINIR
A DEFINIR
A DEFINIR
Contributions bienvenues :
- Ouvrez un ticket décrivant l'amélioration souhaitée.
- Créez une branche dédiée, puis envoyez une Pull Request avec des explications et tests si nécessaire.
Avant une PR :
- Documentez la fonctionnalité
- Ajoutez des exemples et tests (si vous ajoutez des prédicats)
- W. Bibel, "An approach to a systematic theorem proving procedure in first-order logic", Computing, vol. 12, pp. 43–55, 1974
- W. Bibel, Automated Theorem Proving, Vieweg+Teubner Verlag, 1982 (2e éd. 1987)
- L. A. Wallen, Automated Proof Search in Non-Classical Logics: Efficient Matrix Proof Methods for Modal and Intuitionistic Logics, MIT Press, 1990
- Cours M1 Preuves & déductions automatisées — Didier Galmiche, Université de Lorraine
Ce projet est distribué sous la licence MIT. Voir le fichier LICENSE pour le texte complet de la licence.
PiTuring & Metheor31Game — Implementation pédagogique et didactique — M1 S8, Master Informatique, Université de Lorraine.
