Debian Science Project
Summary
Logic
pacchetti Debian Science per la logica

Questo metapacchetto fa parte del Debian Pure Blend "Debian Science" e installa i pacchetti relativi alla logica computazionale. Contiene strumenti per trasformazioni di formule, risolutori per formule specificate in varie logiche, sistemi di dimostrazione interattivi, ecc.

Description

For a better overview of the project's availability as a Debian package, each head row has a color code according to this scheme:

If you discover a project which looks like a good candidate for Debian Science to you, or if you have prepared an unofficial Debian package, please do not hesitate to send a description of that project to the Debian Science mailing list

Links to other tasks

Debian Science Logic packages

Official Debian packages with high relevance

Agda
linguaggio di programmazione funzionale tipizzato in modo dipendente
Versions of package agda
ReleaseVersionArchitectures
wheezy2.3.0.1-2all
jessie2.4.0.2-2all
sid2.6.0.1-1all
bullseye2.6.0.1-1all
buster2.5.4.1-3all
stretch2.5.1.1-3all
Debtags of package agda:
rolemetapackage
Popcon: 0 users (0 upd.)*
Versions and Archs
License: DFSG free
Git

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
dimostratore automatico di teoremi dedicato alla verifica dei programmi
Versions of package alt-ergo
ReleaseVersionArchitectures
bullseye2.0.0-5amd64,arm64,armel,i386,mips64el,mipsel,ppc64el,s390x
stretch1.30-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
squeeze0.91-2amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy0.94-2amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie0.95.2-3amd64,armel,armhf,i386
sid2.0.0-5amd64,arm64,armel,i386,mips64el,mipsel,ppc64el,s390x
buster2.0.0-3amd64,arm64,armel,i386,mips,mips64el,mipsel,ppc64el,s390x
Debtags of package alt-ergo:
roleprogram
uitoolkitgtk
Popcon: 10 users (17 upd.)*
Versions and Archs
License: DFSG free
Git

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, così come l'interfaccia grafica.

Boolector
risolutore SMT per vettori di bit e array
Maintainer: Michael Tautschnig
Versions of package boolector
ReleaseVersionArchitectures
wheezy1.4.ffc2089.100608-1amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie1.5.118.6b56be4.121013-1amd64,armel,armhf,i386
sid1.5.118.6b56be4.121013-1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
buster1.5.118.6b56be4.121013-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch1.5.118.6b56be4.121013-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye1.5.118.6b56be4.121013-1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
squeeze1.4.ffc2089.100608-1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
Debtags of package boolector:
roleprogram
Popcon: 6 users (1 upd.)*
Versions and Archs
License: DFSG free

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
risolutore di insiemi di risposte per apprendimento nogood pilotato dai conflitti
Versions of package clasp
ReleaseVersionArchitectures
jessie3.1.0-1amd64,armel,armhf,i386
wheezy2.0.6-2amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
sid3.3.4-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bullseye3.3.4-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
buster3.3.4-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch3.2.1-3amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
upstream3.3.5
Debtags of package clasp:
roleprogram
Popcon: 66 users (45 upd.)*
Newer upstream!
License: DFSG free
Git

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

Coala
traduce linguaggi di azioni in programmi per insieme di risposte
Versions of package coala
ReleaseVersionArchitectures
jessie1.0.1-5amd64,armel,armhf,i386
wheezy1.0.1-5amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
Debtags of package coala:
roleprogram
Popcon: 0 users (0 upd.)*
Versions and Archs
License: DFSG free
Git

Lo strumento coala traduce un linguaggio di azioni in un programma di logica sotto la semantica di insiemi di risposte. Dopo essere stato scomposto negli elementi base da lparse o gringo, il programma di logica può essere risolto da un risolutore per insieme di risposte come clasp. Attualmente coala è in grado di tradurre i linguaggi di azioni AL, B, C, un sottoinsieme di C+ e il linguaggio d'azioni CTAID. Il tipo del linguaggio di input può essere specificato con un'opzione sulla riga di comando.

Coinor-cbc
risolutore Coin-or per programmazione intera mista branch-and-cut
Versions of package coinor-cbc
ReleaseVersionArchitectures
sid2.9.9+repack1-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
buster2.9.9+repack1-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch2.8.12-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie2.8.12-1amd64,armel,armhf,i386
bullseye2.9.9+repack1-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
upstream2.10.3
Popcon: 86 users (33 upd.)*
Newer upstream!
License: DFSG free
Git

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.

Coinor-symphony
COIN-OR solver for mixed-integer linear programs
Versions of package coinor-symphony
ReleaseVersionArchitectures
buster5.6.16+repack1-1.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie5.6.1-1amd64,armel,armhf,i386
stretch5.6.1-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye5.6.16+repack1-1.1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
sid5.6.16+repack1-1.1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
upstream5.6.17
Popcon: 18 users (4 upd.)*
Newer upstream!
License: DFSG free
Git

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
assistente alle dimostrazioni per logiche di ordine superiore (toplevel e compilatore)
Versions of package coq
ReleaseVersionArchitectures
sid8.9.1-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bullseye8.9.1-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
squeeze8.2.pl2+dfsg-1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy8.3.pl4+dfsg-2amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie8.4pl4dfsg-1amd64,armel,armhf,i386
buster8.9.0-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch8.6-4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
upstream8.10.2
Debtags of package coq:
develcompiler
fieldmathematics
interfacecommandline, text-mode
roleprogram
scopeutility
uitoolkitncurses
Popcon: 48 users (53 upd.)*
Newer upstream!
License: DFSG free
Git

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.

Il pacchetto proofgeneral permette di modificare le dimostrazioni con Emacs e XEmacs.

The package is enhanced by the following packages: libaac-tactics-ocaml libssreflect-ocaml
Cvc3
Automatic theorem prover for SMT problems
Maintainer: Morgan Deters (Adrian Bunk)
Versions of package cvc3
ReleaseVersionArchitectures
wheezy2.4.1-4amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie2.4.1-5amd64,armel,armhf,i386
stretch2.4.1-5.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
squeeze2.2-13amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
Debtags of package cvc3:
interfacecommandline
roleprogram
Popcon: 5 users (0 upd.)*
Versions and Archs
License: DFSG free

CVC3 is an automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination.

CVC3 is the last offspring of a series of popular SMT provers, which originated at Stanford University with the SVC system. In particular, it builds on the code base of CVC Lite, its most recent predecessor. Its high level design follows that of the Sammy prover.

CVC3 works with a version of first-order logic with polymorphic types and has a wide variety of features including:

  • several built-in base theories: rational and integer linear arithmetic, arrays, tuples, records, inductive data types, bit vectors, and equality over uninterpreted function symbols;
  • support for quantifiers;
  • an interactive text-based interface;
  • rich C, C++, and Java APIs for embedding in other systems;
  • proof and model generation abilities;
  • predicate subtyping;
  • essentially no limit on its use for research or commercial purposes (see license).

This package contains the CVC3 command line program.

The package is enhanced by the following packages: cvc3-el
Cvc4
dimostratore automatico di teoremi per problemi SMT
Versions of package cvc4
ReleaseVersionArchitectures
buster1.6-2amd64,i386,mips,mips64el,mipsel
bullseye1.6-2amd64,i386,mips64el,mipsel
sid1.6-2amd64,i386,mips64el,mipsel
Popcon: 8 users (5 upd.)*
Versions and Archs
License: DFSG free
Git

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
solver for quantified boolean formulae
Versions of package depqbf
ReleaseVersionArchitectures
buster5.01-3amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye5.01-3amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
sid5.01-3amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
jessie3.04-1amd64,armel,armhf,i386
wheezy0.1-1amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
stretch5.01-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
upstream6.03
Popcon: 6 users (2 upd.)*
Newer upstream!
License: DFSG free
Git

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.

Gringo
strumenti di grounding per programmi di logica (disgiuntiva)
Versions of package gringo
ReleaseVersionArchitectures
wheezy3.0.4-3amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie4.4.0-1amd64,armel,armhf,i386
stretch5.1.0-4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster5.3.0-10amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye5.3.0-10amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
sid5.3.0-10amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
upstream5.4.0
Debtags of package gringo:
roleprogram
Popcon: 75 users (43 upd.)*
Newer upstream!
License: DFSG free
Git

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.
Please cite: Martin Gebser, Roland Kaminski, Benjamin Kaufmann and Torsten Schaub: Multi-shot ASP solving with clingo. Theory and Practice of Logic Programming :1–56 (2018)
Hol-light
HOL Light theorem prover
Versions of package hol-light
ReleaseVersionArchitectures
sid20190729-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
wheezy20120602-1amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie20131026-1amd64,armel,armhf,i386
stretch20170109-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Popcon: 2 users (0 upd.)*
Versions and Archs
License: DFSG free
Git

HOL Light is an interactive theorem prover for Higher-Order Logic with a very simple logical core running in an OCaml toplevel. HOL Light is famous for the verification of floating-point arithmetic as well as for the Flyspeck project, which aimed at the formalization of Tom Hales' proof of the Kepler conjecture.

Hol88
Higher Order Logic, immagine del sistema
Maintainer: Camm Maguire
Versions of package hol88
ReleaseVersionArchitectures
buster2.02.19940316-35amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie2.02.19940316-28amd64,armel,armhf,i386
bullseye2.02.19940316-35amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
stretch2.02.19940316-33amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
squeeze2.02.19940316-13.1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy2.02.19940316-15amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
sid2.02.19940316-35amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
Debtags of package hol88:
uitoolkitncurses
Popcon: 5 users (3 upd.)*
Versions and Archs
License: DFSG free

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.

Lbt
convertitore di formule LTL in automi di Büchi
Versions of package lbt
ReleaseVersionArchitectures
sid1.2.2-6amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
wheezy1.2.2-5amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
squeeze1.2.2-4amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
jessie1.2.2-5amd64,armel,armhf,i386
stretch1.2.2-6amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster1.2.2-6amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye1.2.2-6amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
Debtags of package lbt:
fieldmathematics
interfacecommandline
roleprogram
scopeutility
useconverting
Popcon: 6 users (5 upd.)*
Versions and Archs
License: DFSG free
Git

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

Mace2
programma che ricerca modelli finiti di dichiarazioni di primo ordine
Versions of package mace2
ReleaseVersionArchitectures
jessie3.3f-1.1amd64,armel,armhf,i386
squeeze3.3f-1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy3.3f-1.1amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
Debtags of package mace2:
roleprogram
usesearching
Popcon: 0 users (0 upd.)*
Versions and Archs
License: DFSG free

MACE è un programma che ricerca i modelli finiti di dichiarazioni di primo ordine e di equazioni sviluppato presso l'Argonne National Laboratory.

Questo pacchetto include ANLDP, che chiama la procedura decisionale proposizionale direttamente al nucleo centrale di MACE.

MACE funziona come compagno complementare per OTTER, che ricerca confutazioni della stessa classe di dichiarazione. In particolare, se si ha una congettura di primo ordine, OTTER ricercherà una prova, e MACE ricercherà un contro esempio dallo stesso file di ingresso.

Maria
analizzatore di raggiungibilità per reti ASN (Algebraic System Nets)
Versions of package maria
ReleaseVersionArchitectures
stretch1.3.5-4.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
sid1.3.5-4.1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
squeeze1.3.5-2amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy1.3.5-4amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
bullseye1.3.5-4.1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
buster1.3.5-4.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie1.3.5-4amd64,armel,armhf,i386
Debtags of package maria:
develtesting-qa
fieldmathematics
interfacetext-mode
roleprogram
scopeutility
uitoolkitncurses
Popcon: 7 users (6 upd.)*
Versions and Archs
License: DFSG free
Git

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.

Matita
strumento per dimostrazione interattiva di teoremi
Versions of package matita
ReleaseVersionArchitectures
stretch0.99.3-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
wheezy0.99.1-1amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
squeeze0.5.8-2amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
sid0.99.3-1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
jessie0.99.1-3amd64,armel,armhf,i386
Debtags of package matita:
fieldmathematics
interfacecommandline, x11
roleprogram
uitoolkitgtk
usechecking
x11application
Popcon: 10 users (0 upd.)*
Versions and Archs
License: DFSG free
Git

Matita è uno strumento grafico interattivo per la dimostrazione di teoremi basato sul calcolo delle costruzioni (co)induttive.

Screenshots of package matita
Maude
infrastruttura logica ad alte prestazioni
Versions of package maude
ReleaseVersionArchitectures
jessie2.6-6amd64,armel,armhf,i386
wheezy2.6-2amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
bullseye2.7-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
sid2.7-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
buster2.7-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch2.7-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Debtags of package maude:
uitoolkitncurses
Popcon: 5 users (3 upd.)*
Versions and Archs
License: DFSG free
Git

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.

Please cite: M. Matsumoto and T. Nishimura: Mersenne Twister: A 623-Dimensionally Equidistributed Uniform Pseudo-Random Number Generator. ACM Transactions on Modeling and Computer Simulation 8(1):3-30 (1998)
Minisat+
risolutore per vincoli pseudo-booleani
Versions of package minisat+
ReleaseVersionArchitectures
bullseye1.0-4amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
wheezy1.0-2amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
sid1.0-4amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
jessie1.0-2amd64,armel,armhf,i386
stretch1.0-3amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster1.0-4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Debtags of package minisat+:
fieldmathematics
roleprogram
Popcon: 5 users (2 upd.)*
Versions and Archs
License: DFSG free
Git

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
dimostratore di teoremi basato su automi
Versions of package mona
ReleaseVersionArchitectures
squeeze1.4-13-1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
buster1.4-17-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch1.4-17-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie1.4-15-1amd64,armel,armhf,i386
wheezy1.4-13-3amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
sid1.4-17-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bullseye1.4-17-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
Debtags of package mona:
fieldmathematics
roleprogram
scopeutility
Popcon: 8 users (2 upd.)*
Versions and Archs
License: DFSG free
Git

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

Picosat
risolutore SAT con gestione di dimostrazione e nucleo
Versions of package picosat
ReleaseVersionArchitectures
stretch960-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie960-1amd64,armel,armhf,i386
wheezy936-4amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
squeeze913-4amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
sid965-1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bullseye965-1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
buster960-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Debtags of package picosat:
fieldmathematics
roleprogram
Popcon: 11 users (0 upd.)*
Versions and Archs
License: DFSG free
Git

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.

Screenshots of package picosat
Proofgeneral
frontend generico per assistenti alla dimostrazione
Versions of package proofgeneral
ReleaseVersionArchitectures
sid4.4.1~pre170114-1.1all
jessie4.3~pre131011-0.2all
squeeze3.7-4all
wheezy4.2~pre120605-2all
stretch4.4.1~pre170114-1all
Debtags of package proofgeneral:
fieldmathematics
interfacetext-mode, x11
roleplugin
suiteemacs
useediting
Popcon: 12 users (8 upd.)*
Versions and Archs
License: DFSG free

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

Other screenshots of package proofgeneral
VersionURL
4.3~pre130510-1.1https://screenshots.debian.net/screenshots/000/012/105/large.png
Screenshots of package proofgeneral
Prover9
strumento per dimostrazione di teoremi e generazione di contromodelli
Versions of package prover9
ReleaseVersionArchitectures
squeeze0.0.200902a-2amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
jessie0.0.200911a-2.1amd64,armel,armhf,i386
stretch0.0.200911a-2.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster0.0.200911a-2.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
wheezy0.0.200902a-2.1amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
Popcon: 36 users (10 upd.)*
Versions and Archs
License: DFSG free
Bzr

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.

Sat4j
libreria efficiente per solutori SAT in Java
Versions of package sat4j
ReleaseVersionArchitectures
bullseye2.3.5-0.3all
stretch2.3.5-0.2all
jessie2.3.3-1all
squeeze2.2.0-3all
wheezy2.3.1-1all
sid2.3.5-0.3all
buster2.3.5-0.3all
Debtags of package sat4j:
fieldmathematics
roleprogram, shared-lib
Popcon: 209 users (47 upd.)*
Versions and Archs
License: DFSG free

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
verificatore automatico di teoremi per logica del primo ordine con uguaglianza
Versions of package spass
ReleaseVersionArchitectures
squeeze3.7-2amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
stretch3.7-4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
sid3.7-4amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
wheezy3.7-3amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie3.7-3amd64,armel,armhf,i386
Debtags of package spass:
fieldmathematics
Popcon: 5 users (0 upd.)*
Versions and Archs
License: DFSG free
Git

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
ottimizzazione combinatoriale esatta per modelli grafici
Versions of package toulbar2
ReleaseVersionArchitectures
buster1.0.0+dfsg3-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye1.0.0+dfsg3-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
sid1.0.0+dfsg3-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
Popcon: 7 users (4 upd.)*
Versions and Archs
License: DFSG free
Git

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.

Why
strumento di verifica del software
Versions of package why
ReleaseVersionArchitectures
wheezy2.30+dfsg-5amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie2.34-2amd64,armel,armhf,i386
squeeze2.26+dfsg-2+squeeze1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
Debtags of package why:
develtesting-qa
roleprogram
Popcon: 0 users (1 upd.)*
Versions and Archs
License: DFSG free
Git

Lo scopo di Why è essere un back-end per VCG (generatore di condizioni di verifica) per altri strumenti di verifica. Fornisce un potente linguaggio per l'input che include funzioni di ordine superiore, polimorfismo, riferimenti, array ed eccezioni. Genera prove per molti sistemi: i sistemi di dimostrazione assistita Coq, PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar e le procedure di decisione Simplify, Alt-Ergo, Yices, CVC Lite e haRVey.

Screenshots of package why
Why3
piattaforma di verifica del software
Versions of package why3
ReleaseVersionArchitectures
buster1.2.0-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye1.2.1-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
stretch0.87.3-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
sid1.2.1-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
Popcon: 9 users (10 upd.)*
Versions and Archs
License: DFSG free
Git

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
dimostratore di teoremi di Microsoft Research
Versions of package z3
ReleaseVersionArchitectures
stretch4.4.1-1~deb9u1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
sid4.8.7-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bullseye4.8.6-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
buster4.4.1-1~deb10u1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Popcon: 21 users (38 upd.)*
Versions and Archs
License: DFSG free
Git

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.

Official Debian packages with lower relevance

Coinor-libcoinmp-dev
Simple C API for COIN-OR Solvers Clp and Cbc -- development
Versions of package coinor-libcoinmp-dev
ReleaseVersionArchitectures
buster1.8.3-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch1.7.6+dfsg1-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie1.7.6+dfsg1-1amd64,armel,armhf,i386
sid1.8.3-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bullseye1.8.3-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
Popcon: 6 users (6 upd.)*
Versions and Archs
License: DFSG free

The Coin-MP optimizer is an open source solver, it is part of the COIN-OR project which is an initiative to spur the development of open-source software for the operations research community.

CoinMP is a C-API library that supports most of the functionality of CLP (Coin LP), CBC (Coin Branch-and-Cut), and CGL (Cut Generation Library) projects.

This package contains the files needed to build applications using libCoinMP.

*Popularitycontest results: number of people who use this package regularly (number of people who upgraded this package recently) out of 202987