Paquet : prover9 (0.0.200911a-2.1 et autres)

[ Paquet source : ladr  ]

démonstrateur de théorème et générateur de contre-exemples

Ce paquet fournit le démonstrateur de théorème de résolution et « paramodulation » Prover9 et le générateur de contre-exemples Mace4.

Prover9 est un démonstrateur de théorème automatique de calcul des prédicats du premier ordre. C’est un successeur du démonstrateur Otter. Prover9 utilise les techniques d’inférence de résolution et paramodulation ordonnées avec sélection de littéraux.

Le programme Mace4 recherche des modèles finis satisfaisant des propositions d’équation du premier ordre, du même genre que celles que Prover9 accepte. Si la proposition est la négation d’une conjecture, tout modèle trouvé par Mace4 est un contre-exemple de cette conjecture.

Mace4 peut être un complément précieux à Prover9, recherchant des contre-exemples avant (ou simultanément) l’utilisation de Prover9 pour la recherche de preuve. Il peut aussi être utilisé pour aider à déboguer des propositions et formules d’entrée pour Prover9.

Autres paquets associés à prover9

• dep: libc6 (>= 2.17) [arm64]

  bibliothèque C GNU : bibliothèques partagées
  un paquet virtuel est également fourni par libc6-udeb

  dep: libc6 (>= 2.7) [non arm64]

• dep: libladr4 (>= 0.0.200911a-1)

  bibliothèque de déduction LADR

• sug: ladr4-apps (= 0.0.200911a-2.1+b2)

  bibliothèque de déduction LADR – diverses applications

• sug: prover9-doc (<< 0.0.200902b)

  documentation pour Prover9 et programmes associés.

  sug: prover9-doc (>> 0.0.200902a)

Télécharger prover9

Télécharger pour toutes les architectures proposées

Architecture	Version	Taille du paquet	Espace occupé une fois installé	Fichiers
amd64	0.0.200911a-2.1+b2	100,4 ko	303,0 ko	[liste des fichiers]
arm64	0.0.200911a-2.1+b2	90,6 ko	297,0 ko	[liste des fichiers]
armhf	0.0.200911a-2.1+b2	94,3 ko	245,0 ko	[liste des fichiers]
i386	0.0.200911a-2.1+b2	106,8 ko	303,0 ko	[liste des fichiers]