Paquet : minlog (4.0.99.20100221-7)

système de manipulation de preuve basé sur des calculs de déduction naturelle du premier ordre

destiné à raisonner sur des fonctions calculables en utilisant une logique minimale plutôt que classique ou intuitive. La motivation principale derrière MINLOG est d'exploiter le paradigme de « preuve comme programme » pour le développement de programmes et la vérification de programmes. Les preuves sont en réalité traitées comme objets de première classe qui peuvent être normalisés. Si une formule est existentielle alors sa preuve peut être utilisée pour en lire une instance, ou modifiée de manière appropriée pour le développement de programme par transformation de preuves. Pour cela, MINLOG est doté d'outils pour extraire des programmes fonctionnels directement des termes de preuve. Cela s'applique également aux preuves non constructives, en utilisant une translation A affinée. Le système est basé sur une recherche automatique de preuves et une normalisation par évaluation en tant que terminal efficace de réécriture de terme.

Minilog peut être utilisé avec ProofGeneral, qui permet aux preuves d'être éditée avec emacs ou xemacs. Cela nécessite que le paquet proofgeneral- minlog soit installé.

Cette page est uniquement disponible dans les langues suivantes (Comment configurer la langue par défaut du document) :