toutes les options
jessie  ] [  stretch  ] [  buster  ] [  bullseye  ] [  sid  ]
[ Paquet source : minlog  ]

Paquet : minlog (4.0.99.20100221-6)

Liens pour minlog

Screenshot

Ressources Debian :

Télécharger le paquet source minlog :

Responsable :

Ressources externes :

Paquets similaires :

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é.

Autres paquets associés à minlog

  • dépendances
  • recommandations
  • suggestions
  • enhances

Télécharger minlog

Télécharger pour toutes les architectures proposées
Architecture Taille du paquet Espace occupé une fois installé Fichiers
all 2 568,0 ko7 555,0 ko [liste des fichiers]