918.tex

\documentclass{agregfiche}

\title{Leçon 918 - Systèmes formels de preuve en logique du premier ordre. Exemples.}

% V1 par Charlie Jacomme
% Relu par Sylvain Schmitz


\begin{document}
\maketitle

\secrapports
\begin{rapport}{2017,2018,2019}
	Le jury attend du candidat qu’il présente au moins la déduction naturelle ou un calcul de séquents
	et qu’il soit capable de développer des preuves dans ce système sur des exemples classiques simples.
	La présentation des liens entre syntaxe et sémantique, en développant en particulier les questions de
	correction et complétude, et de l’apport des systèmes de preuves pour l’automatisation des preuves est
	également attendue.
	Le jury appréciera naturellement si des candidats présentent des notions plus élaborées comme la
	stratégie d’élimination des coupures mais est bien conscient que la maîtrise de leurs subtilités va au-
	delà du programme.
\end{rapport}

\secindispensables

\begin{itemize}
	\item Un système de preuve, et des preuves.
	\item Syntaxe et Sémantique, correction et complétude.
\end{itemize}

\secasavoir

\begin{itemize}
	\item Calcul des séquents, déduction naturelle.
	\item Algorithme d'unification.
	\item Preuves par résolution.
	\item Automatisation des preuves.
\end{itemize}

\secidees

\begin{itemize}
	\item Élimination des coupures.
	\item Logique intuitionniste.
	\item Compacité.
	\item Méthodes des tableaux.
	\item Théories équationelle et réécriture.
	\item Clauses de Horn, résolution et Prolog.
\end{itemize}

\secpieges

\begin{itemize}
    \item Il faut au moins deux systèmes différents. Trois, c'est trop.
	\item Éviter de mettre les règles du système principal en annexes. Des arbres de preuves peuvent y trouver leur place.
	\item Ne pas mettre tous les systèmes. Attention à bien justifier l'introduction des différents systèmes, on ne fait pas un catalogue.
    \item Les formules sont des termes, pas des mots avec parenthèses (pourquoi pas la notation polonaise inverse tant qu'on y est !)
    \item Ne pas proposer la correction en développement.
	\item Cette leçon ne porte pas sur les théories.
    \item La théorie de l'égalité peut apparaître comme une théorie, mais il vaut mieux éviter de la mettre directement dans le système de preuve.
    \item Attention à la notion d'$\alpha$-renommage, dur à définir
    complètement correctement.
        \item Se méfier de la déduction naturelle, c'est difficile de
        l'utiliser sur des exemples.
\end{itemize}

\secquestionsclassiques

\begin{itemize}
    \item Telle règle pourrait-elle être écrite différemment/est-elle admissible ?
	\item Discuter des difficultés de l'automatisation dans
	différents systèmes.
%    problème de choix
	\item Démontrer telle formule dans tel système.
	\item La logique du premier ordre est-elle décidable ?
% non   , via PCP
	\item Motivation derrière le développements des systèmes à la
	Hilbert ?
% formalisation des preuves
	\item Connaissez vous des outils (programmes) permettant de
	travailler avec un système de preuve et faire des preuves
	formelles ?
%     Coq, HOL, Isabelle

\end{itemize}

\secreferences

\begin{itemize}
\item \input{refs/goubault}
\item \input{refs/david}
\item \input{refs/dowek}



\end{itemize}

\secdev

\begin{itemize}
\item Le théorème de \bsc{Herbrand } est hors-sujet, c'est de la sémantique.
\item L'unification est vraiment border line.
\item L'élimination des coupures est trop dur à faire passer dans le temps.
\item[++] \input{dev/comp}
\item[++] \input{dev/contraction}
\item Développement d'un exemple de preuve en déduction naturelle ou en calcul des séquents.
\end{itemize}


\end{document}