Questo è il comando prover9 che può essere eseguito nel provider di hosting gratuito OnWorks utilizzando una delle nostre molteplici workstation online gratuite come Ubuntu Online, Fedora Online, emulatore online Windows o emulatore online MAC OS
PROGRAMMA:
NOME
prover9 - teorema di risoluzione/paramodulazione prover
SINOSSI
prover9 [Opzioni] file di input > file di uscita
prover9 [Opzioni] -F file di input > file di uscita
DESCRIZIONE
Questa pagina di manuale documenta brevemente il prover9 comando.
prover9 è un dimostratore di teoremi automatizzato per logica del primo ordine ed equazionale. È un
successore del lontra(1) sperimentatore. prover9 utilizza le tecniche di inferenza dell'ordinato
risoluzione e paramodulazione con selezione letterale.
VERSIONI
Di seguito è riportato un riepilogo delle opzioni.
-h Visualizza un elenco di opzioni della riga di comando.
-x Abilita una modalità automatica avanzata sperimentale. Per maggiori informazioni consultare il
prover9 manuale.
-p Uscita tra parentesi completamente.
-t n Limita la ricerca a durare circa n secondi. Per i sistemi simili a UNIX, l'"utente"
Viene utilizzato il tempo della CPU.
-f filetto
Prendi input da filetto invece che dall'input standard.
Usa prover9 online utilizzando i servizi onworks.net
