Package: prover9 (0.0.200911a-2.1 and others)

[ Source: ladr  ]

strumento per dimostrazione di teoremi e generazione di contromodelli

Questo pacchetto fornisce lo strumento di dimostrazione con risoluzione/paramodulazione di teoremi Prover9 e il generatore di contromodelli Mace4.

Prover9 è uno strumento automatico per la dimostrazione di teoremi del primo ordine e di logica equazionale. È un successore del dimostratore Otter. Prover9 usa le tecniche di inferenza di risoluzioni ordinate e la paramodulazione con selezione di letterali.

Il programma Mace4 cerca strutture finite che soddisfino le dichiarazioni di primo ordine e delle equazioni, lo stesso tipo di dichiarazioni che accetta Prover9. Se la dichiarazione è la negazione di una qualche congettura, qualsiasi struttura trovata da Mace4 è un controesempio per la congettura.

Mace4 può essere un complemento di gran valore per Prover9 che cerca controesempi prima (o nello stesso momento) dell'utilizzo di Prover9 per cercare una dimostrazione. Può anche essere usato per aiutare a fare il debug delle clausole in input e delle formule per Prover9.

Other Packages Related to prover9

• dep: libc6 (>= 2.17)

  Libreria C GNU: librerie condivise
  also a virtual package provided by libc6-udeb

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

  libreria per deduzioni LADR

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

  libreria per deduzioni LADR - applicazioni varie

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

  documentazione per Prover9 e programmi associati

  sug: prover9-doc (>> 0.0.200902a)

Download prover9

Download for all available architectures

Architecture	Version	Package Size	Installed Size	Files
arm64	0.0.200911a-2.1+b2	90.6 kB	297.0 kB	[list of files]