Debian Science Logic packages

Agda è un linguaggio di programmazione funzionale tipizzato in modo dipendente: ha famiglie induttive che sono simili alle GADT di Haskell, ma possono essere indicizzate in base ai valori e non soltanto ai tipi. Ha anche moduli parametrizzati, operatori mixfix, caratteri Unicode e un'interfaccia Emacs interattiva (il verificatore dei tipi può assistere nella scrittura del codice).

Agda è anche un assistente per dimostrazioni: è un sistema interattivo per scrivere e verificare dimostrazioni. Agda è basato sulla teoria intuizionista dei tipi, un sistema fondante per lo sviluppo della matematica costruttiva creata dal logico svedese Per Martin-Löf. Ha molte similitudini con altri assistenti per dimostrazioni basati su tipi dipendenti, come Coq, Epigram e NuPRL.

Questo è un metapacchetto che fornisce la documentazione, la libreria standard, l'eseguibile, la modalità Emacs di Agda.

Alt-Ergo è un dimostratore automatico di teoremi pensato per l'uso nella verifica dei programmi. È basato su CC(X): un algoritmo di "Congruence Closure" parametrizzato da una teoria di equazioni X. Alter-Ergo ha dimostratori incorporati per logica proposizionale, aritmetica lineare, simboli di funzioni non interpretate, simboli di funzioni associative-commutative, array polimorfi, tipi di record polimorfi definiti dall'utente e tipi per enumerazione polimorfi. Ha una gestione ristretta per il ragionamento su tipi algebrici arbitrari definiti dall'utente, quantificatori del primo ordine e aritmetica non lineare.

Questo pacchetto contiene il dimostratore in forma di eseguibile a riga di comando.

Boolector è un efficiente risolutore SMT per la teoria libera da quantificatori dei vettori di bit in combinazione con la teoria degli array con estensionalità libera da quantificatori.

clasp è un risolutore di insiemi di risposte per programmi di logica normale (estesa). Combina le capacità di modellazione di alto livello di ASP (Answer Set Programming) con tecniche all'avanguardia dall'area della risoluzione di vincoli booleani. L'algoritmo primario di clasp si basa sull'apprendimento nogood pilotato da conflitti, una tecnica che ha dimostrato grande successo per i controlli di soddisfacibilità (SAT). A differenza di altri risolutori ASP con apprendimento, clasp non si basa su software datato, come un risolutore SAT o qualsiasi altro risolutore ASP esistente. Invece clasp è stato sviluppato veramente per la risoluzione di insiemi di risposte basata su apprendimento nogood pilotato da conflitti. clasp può essere applicato come risolutore ASP (sul formato di output LPARSE), come risolutore SAT (su formato DIMACS/CNF semplificato) o come risolutore PB (su formato OPB).

Cbc (Coin-or branch and cut) è un risolutore open-source per programmazione intera mista scritto in C++. Può essere usato come libreria richiamabile o come eseguibile autonomo.

Questo pacchetto contiene l'eseguibile cbc.

SYMPHONY is an open-source generic mixed-integer linear programs (MILP) solver, callable library, and extensible framework for implementing customized solvers SYMPHONY has a number of advanced capabilities, including the ability to solve multi-objective MILPs, the ability to warm start its solution procedure, and the ability to perform basic sensitivity analyses.

SYMPHONY is part of the larger COIN-OR initiative (Computational Infrastructure for Operations Research).

This package contains the symphony executable.

Coq è un assistente alle dimostrazioni per logiche di ordine superiore che permette lo sviluppo di programmi per computer coerenti con la loro specifica formale. È sviluppato con Objective Caml e Camlp5.

Questo pacchetto fornisce coqtop, un'interfaccia a riga di comando per Coq.

Un'interfaccia grafica per Coq è inclusa nel pacchetto coqide. Coq può anche essere usato con ProofGeneral, che permette di modificare le dimostrazioni con emacs e xemacs. Quest'operazione richiede che sia installato il pacchetto proofgeneral.

CVC4 è un efficiente dimostratore automatico di teoremi per problemi SMT (Satisfiability Modulo Theories). Può essere usato per dimostrare la validità (o, in maniera duale, la soddisfacibilità) di formule del primo ordine per un grande numero di teorie logiche incorporate e di loro combinazioni.

CVC4 è pensato per essere un motore SMT aperto ed estensibile e può essere usato come strumento autonomo o come libreria. È il quarto nella famiglia di strumenti Cooperating Validity Checker (che include anche CVC, CVC Lite e CVC3). CVC4 è stato progettato per aumentare le prestazioni e ridurre l'uso di memoria dei suoi predecessori.

Questo pacchetto contiene i binari necessari per usare CVC4 come strumento autonomo.

DepQBF is a search-based solver for quantified boolean formulae (QBF) in prenex conjunctive normal form. It is based on the DPLL algorithm for QBF, called QDPLL, with conflict-driven clause and solution-driven cube learning. By analyzing the syntactic structure of a formula, DepQBF tries to identify independent variables. In general, information on independent variables can be represented in the formal framework of dependency schemes. DepQBF computes the so-called "standard dependency scheme" of a given formula. In addition to other benefits, information on independent variables often increases the freedom for decision making and clause learning.

I risolutori di insiemi di risposte attuali lavorano su programmi liberi da variabili. Perciò è necessario uno strumento di grounding che, dato un programma di input con variabili del primo ordine, calcoli un programma ground equivalente (libero da variabili).

Questo pacchetto contiene i seguenti strumenti:

• gringo: uno strumento di grounding che, dato un programma di input con variabili del primo ordine, calcola un programma ground equivalente (libero da variabili) in formato aspif. Il suo output può essere elaborato ulteriormente con il risolutore di insiemi di risposte clasp. A partire da gringo serie 5, il suo output non è più direttamente compatibile con i risolutori come smodels o cmodels che leggono il formato smodels. Usare lpconvert per tradurre il formato aspif in formato smodels;
• clingo: combina clasp e gringo in un sistema monolitico. In questo modo offre più controllo sui processi di grounding e di soluzione di quanto non offrano gringo e clasp individualmente: soluzioni multi-shot;
• lpconvert: convertitore tra il formato smodels e aspif di gringo;
• reify: piccola utilità che reifica un programma logico fornito in formato aspif. Produce un insieme di fatti che possono essere elaborati ulteriormente con gringo.

HOL Light è un dimostratore interattivo di teoremi per logica di ordine superiore (Higher-Order Logic) con un nucleo logico molto semplice in esecuzione su un livello superiore OCaml. HOL Light è famoso per la verifica di aritmetica a virgola mobile e per il progetto Flyspeck, che aveva come obiettivo la formalizzazione della dimostrazione di Tom Hales della congettura di Keplero.

Il sistema HOL è un ambiente per la dimostrazione interattiva di teoremi in una logica di ordine superiore (Higher-Order Logic). La sua caratteristica più degna di nota è il suo alto grado di programmabilità attraverso il metalinguaggio ML. Il sistema ha una vasta gamma di utilizzi, dalla formalizzazione di matematica pura alla verifica di hardware industriale. Siti accademici e industriali in tutto il mondo usano HOL.

Questo software converte una formula logica temporale lineare (ltl) in un automa di Büchi generalizzato. L'automa risultante si può usare, per esempio, nel controllo di modelli, dove rappresenta una proprietà che debba essere verificata da un modello (per esempio una rete di Petri).

Maria è un potente strumento pensato per aiutare i progettisti a modellare e risolvere i problemi legati alla concorrenza su sistemi paralleli e distribuiti.

Esplorando tutti gli stati raggiungibili dallo stato iniziale di un sistema, Maria trova le condizioni di stallo e le violazioni dei requisiti di sicurezza o di "liveness". Può gestire decine o centinaia di milioni di stati raggiungibili e azioni abilitate.

Il potere espressivo del formalismo usato da Maria è vicino a quello dei linguaggi di programmazione ad alto livello, grazie alla sua ricchezza di tipi e alle potenti operazioni algebriche.

Maude è un linguaggio riflessivo e un sistema ad alte prestazioni che gestisce la specificazione di logica sia equazionale sia con riscrittura e la programmazione per una vasta gamma di applicazioni. Maude è stato influenzato in modo importante dal linguaggio OBJ3 che può essere considerato un sottolinguaggio di logica equazionale. Oltre a gestire la specificazione e la programmazione equazionale, Maude gestisce anche il calcolo con logica con riscrittura.

La logica con riscrittura è una logica di cambiamento concorrente che può naturalmente affrontare stati e calcoli concorrenti. Ha buone proprietà come infrastruttura semantica generica per fornire semantiche eseguibili ad una vasta gamma di linguaggi e modelli di concorrenza. In particolare, gestisce molto bene calcoli concorrenti orientati agli oggetti. Questi stessi motivi fanno della logica con riscrittura una buona infrastruttura logica, cioè una metalogica in cui molte altre logiche possono essere naturalmente rappresentate ed eseguite.

Maude gestisce in modo sistematico ed efficiente la riflessione logica. Ciò rende Maude particolarmente estensibile e potente, gestisce un'algebra estensibile di operazione di composizione di moduli e permette molte applicazioni avanzate di metaprogrammazione e metalinguaggio. Difatti, alcune delle applicazioni più interessanti di Maude sono applicazioni con metalinguaggi, in cui Maude viene usato per creare ambienti eseguibili per logiche diverse, dimostratori di teoremi, linguaggi e modelli di calcolo.

Maude è interessante per la comunità biomedica per fare modelli e analisi di sistemi biologici.

MinSat+ è un risolutore per ottimizzazione pseudo-booleana (alias programmazione 0-1 intera) che è basato sul risolutore SAT MiniSat. Gestisce l'ottimizzazione di una funzione obiettivo lineare, soggetta a un insieme di vincoli lineari. Le variabili della funzione obiettivo e i vincoli sono booleani, cioè è richiesto che siano 0 o 1. L'ottimizzazione pseudo-booleana può essere usata per risolvere molti tipi di problemi di ottimizzazione combinatoria. Questa versione di Minisat+ è compilata con la gestione bignum per i coefficienti dei vincoli.

MONA è uno strumento che traduce formule dalle logiche WS1S o WS2S in automi a stati finiti rappresentati da BDD. Le formule possono esprimere schemi di ricerca, proprietà temporali di sistemi reattivi, vincoli di alberi sintattici, ecc. MONA analizza anche l'automa risultante dalla compilazione e determina se la formula è valida e, in caso contrario, genera un controesempio.

La documentazione è disponibile sul sito di MONA: http://www.brics.dk/mona/.

Nonostante che il problema di soddisfacibilità di formule booleane (SAT) sia NP-completo, i risolutori SAT spesso sono in grado di decidere questo problema in un arco di tempo ragionevole. Dal momento che tutti gli altri problemi NP-completi sono riducibili a SAT, i risolutori sono diventati uno strumento di uso generale per questa classe di problemi.

PicoSAT è un risolutore SAT che su istanze industriali si è dimostrato più veloce di MiniSAT 2.0 e può anche generare dimostrazioni e nuclei in memoria.

Proof General è una modalità principale che trasforma Emacs in un assistente interattivo alla dimostrazione per scrivere dimostrazioni matematiche formali usando diversi dimostratori di teoremi.

Questo pacchetto fornisce a Proof General la gestione per Coq. (Non c'è nessun altro assistente alla dimostrazione che si possa sensatamente supportare.)

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.

Lo scopo della libreria SAT4J è fornire una libreria efficiente per risolutori SAT in Java. Rispetto al progetto OpenSAT, la libreria SAT4J si rivolge a utenti alle prime armi con "scatole nere" SAT, che intendano inglobare le tecnologie SAT nelle proprie applicazioni senza curarsi dei dettagli. Il progetto SAT4J tenta anche di fornire una base di lavoro per ricercatori SAT.

SPASS è un verificatore automatico di teoremi basato sulla saturazione per logica del primo ordine con uguaglianza. È unico per la combinazione del calcolo di superposizione con regole specifiche di inferenza/riduzione per ordinamenti (tipi) e una regola di suddivisione per analisi del caso motivate dalla regola beta dei tableaux analitici e analisi del caso impiegate nella procedura Davis-Putnam. Inoltre SPASS fornisce una sofisticata traduzione della forma normale di clausola.

Questo pacchetto consiste dell'eseguibile SPASS/FLOTTER, documentazione e una piccola raccolta d'esempi. Gli insiemi degli strumenti contengono il verificatore pcs, i traduttori di sintassi dfg2otter e dfg2tptp e il programma dfg2ascii per ottenere stampe ASCII graziose.

Toulbar2 è uno strumento per ottimizzazione discreta esatta per modelli grafici come reti di funzioni di costo, campi casuali di Markov, problemi di soddisfazione di vincoli pesati e reti bayesiane.

Why3 è una piattaforma per la verifica deduttiva di programmi. Fornisce un ricco linguaggio, chiamato WhyML, per la specifica e la programmazione e si appoggia a dimostratori di teoremi esterni, sia automatici sia interattivi, per scaricare condizioni di verifica. Why3 viene fornito con una libreria standard di teorie logiche (aritmetica intera e reale, operazioni booleane, insiemi e mappe, ecc.) e strutture di dati base per programmazione (array, code, tabelle hash, ecc.). L'utente può scrivere direttamente programmi WhyML e ottenere programmi OCaml "corretti per costruzione" attraverso un meccanismo di estrazione automatico. WhyML è utilizzato anche come linguaggio intermedio per la verifica di programmi C, Java o Ada.

Why3 è una reimplementazione completa della precedente piattaforma Why. Tra le nuove funzionalità ci sono: numerose estensioni del linguaggio di input, una nuova architettura per chiamare dimostratori esterni e un'API ben progettata che permette di usare Why3 come libreria software. Un'attenzione importante è stata posta nella modularità e generalità, dando all'utente finale la possibilità di riutilizzare facilmente la formalizzazione di Why3 * di aggiungere la gestione di un nuovo dimostratore esterno, se lo desidera.

Z3 è un dimostratore di teoremi all'avanguardia di Microsoft Research. Può essere usato per verificare la soddisfacibilità di formule logiche su una o più teorie. Z3 offre un corrispettivo convincente per strumenti di verifica e analisi del software, dal momento che molti costrutti software comuni mappano direttamente in teorie gestite.

Il formato di input per Z3 è un'estensione di quello definito dallo standard SMT-LIB 2.0.

L'ottimizzatore Coin-MP è un risolutore open source; fa parte del progetto COIN-OR, che è una iniziativa per stimolare lo sviluppo di software open source per la comunità della ricerca operativa.

CoinMP è una libreria con API C che gestisce la maggior parte delle funzionalità dei progetti CLP (Coin LP), CBC (Coin Branch-and-Cut) e CGL (Cut Generation Library).

Questo pacchetto contiene i file necessari per compilare applicazioni che usano libCoinMP.