Summary
Logic
Pakiety do logiki naukowej w Debianie
Ten metapakiet jest częścią Debian Pure Blend "Debian Science" i
instaluje pakiety związane z logiką obliczeniową. Zawiera narzędzia
do przekształcania formuł, solwery dla formuł określonych w różnych
logikach, interaktywne systemy sprawdzające itp.
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
dependently typed functional programming language
|
Versions of package agda |
Release | Version | Architectures |
trixie | 2.6.3-1 | all |
stretch | 2.5.1.1-3 | all |
buster | 2.5.4.1-3 | all |
bullseye | 2.6.1-1 | all |
bookworm | 2.6.2.2-1.1 | all |
sid | 2.6.3-1 | all |
jessie | 2.4.0.2-2 | all |
upstream | 2.6.4.3 |
Debtags of package agda: |
role | metapackage |
|
License: DFSG free
|
Agda is a dependently typed functional programming language: It has inductive
families, which are like Haskell's GADTs, but they can be indexed by values and
not just types. It also has parameterised modules, mixfix operators, Unicode
characters, and an interactive Emacs interface (the type checker can assist in
the development of your code).
Agda is also a proof assistant: It is an interactive system for writing and
checking proofs. Agda is based on intuitionistic type theory, a foundational
system for constructive mathematics developed by the Swedish logician Per
Martin-Löf. It has many similarities with other proof assistants based on
dependent types, such as Coq, Epigram and NuPRL.
This is a meta package which provides Agda's emacs mode, executable, standard
library and its documentation.
|
|
alt-ergo
Automatic theorem prover dedicated to program verification
|
Versions of package alt-ergo |
Release | Version | Architectures |
stretch | 1.30-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
jessie | 0.95.2-3 | amd64,armel,armhf,i386 |
buster | 2.0.0-3 | amd64,arm64,armel,i386,mips,mips64el,mipsel,ppc64el,s390x |
bullseye | 2.0.0-7 | amd64,arm64,armel,i386,mips64el,mipsel,ppc64el,s390x |
Debtags of package alt-ergo: |
role | program |
uitoolkit | gtk |
|
License: DFSG free
|
Alt-Ergo is an automatic theorem prover geared towards application in
program verification. It is based on CC(X), a congruence closure
algorithm parameterized by an equational theory X. Alt-Ergo has
built-in provers for propositional logic, linear arithmetic,
uninterpreted function symbols, associative-commutative function
symbols, polymorphic arrays, user-defined polymorphic record types
and polymorphic enumeration types. It has restricted support for
reasoning over arbitrary user-defined algebraic types, first-order
quantifiers, and non-linear arithmetic.
This package contains the prover as a command-line executable.
|
|
boolector
SMT solver dla wektorów bitowych i tablic
|
Versions of package boolector |
Release | Version | Architectures |
jessie | 1.5.118.6b56be4.121013-1 | amd64,armel,armhf,i386 |
stretch | 1.5.118.6b56be4.121013-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
buster | 1.5.118.6b56be4.121013-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
bullseye | 1.5.118.6b56be4.121013-1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
sid | 1.5.118.6b56be4.121013-1.3 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
bookworm | 1.5.118.6b56be4.121013-1.3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
trixie | 1.5.118.6b56be4.121013-1.3 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,s390x |
Debtags of package boolector: |
role | program |
|
License: DFSG free
|
Boolector jest wydajnym solverem SMT dla teorii wektorów bitowych bez
kwantyfikatora, w połączeniu z bezstratną, rozszerzającą się teorią macierzy.
|
|
clasp
conflict-driven nogood learning answer set solver
|
Versions of package clasp |
Release | Version | Architectures |
buster | 3.3.4-2 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
sid | 3.3.5-4.2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
trixie | 3.3.5-4.2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,s390x |
bookworm | 3.3.5-4.2 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bullseye | 3.3.5-4 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
stretch | 3.2.1-3 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
jessie | 3.1.0-1 | amd64,armel,armhf,i386 |
Debtags of package clasp: |
role | program |
|
License: DFSG free
|
clasp is an answer set solver for (extended) normal logic
programs. It combines the high-level modeling capacities of answer
set programming (ASP) with state-of-the-art techniques from the area
of Boolean constraint solving. The primary clasp algorithm relies on
conflict-driven nogood learning, a technique that proved very
successful for satisfiability checking (SAT). Unlike other learning
ASP solvers, clasp does not rely on legacy software, such as a SAT
solver or any other existing ASP solver. Rather, clasp has been
genuinely developed for answer set solving based on conflict-driven
nogood learning. clasp can be applied as an ASP solver (on LPARSE
output format), as a SAT solver (on simplified DIMACS/CNF format), or
as a PB solver (on OPB format).
|
|
coala
translates action languages into answer set programs
|
Versions of package coala |
Release | Version | Architectures |
jessie | 1.0.1-5 | amd64,armel,armhf,i386 |
Debtags of package coala: |
role | program |
|
License: DFSG free
|
The coala tool translates an action language into a logic program
under the answer set semantics. After being grounded by lparse or
gringo, the logic program can be solved by an answer set solver such
as clasp. At the moment coala is able to translate the action
language AL, B, C, a subset of C+ and the action language CTAID. The
type of input language can be specified with a command line option.
|
|
coinor-cbc
Coin-or branch-and-cut mixed integer programming solver
|
Versions of package coinor-cbc |
Release | Version | Architectures |
sid | 2.10.11+ds1-2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
jessie | 2.8.12-1 | amd64,armel,armhf,i386 |
stretch | 2.8.12-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
buster | 2.9.9+repack1-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
bullseye | 2.10.5+ds1-3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bookworm | 2.10.8+ds1-1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
trixie | 2.10.11+ds1-2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,s390x |
|
License: DFSG free
|
Cbc (Coin-or branch and cut) is an open-source mixed integer programming
solver written in C++. It can be used as a callable library or as a
stand-alone executable.
This package contains cbc executable.
|
|
coinor-symphony
COIN-OR solver for mixed-integer linear programs
|
Versions of package coinor-symphony |
Release | Version | Architectures |
jessie | 5.6.1-1 | amd64,armel,armhf,i386 |
sid | 5.6.17+dfsg-1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
trixie | 5.6.17+dfsg-1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,s390x |
bookworm | 5.6.17+dfsg-1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bullseye | 5.6.16+repack1-3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
buster | 5.6.16+repack1-1.1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
stretch | 5.6.1-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
|
License: DFSG free
|
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
Asystent udowadniania logiki wyższego rzędu (interfejs i kompilator)
|
Versions of package coq |
Release | Version | Architectures |
sid | 8.18.0+dfsg-1 | amd64,arm64,armhf,i386,ppc64el,riscv64,s390x |
trixie | 8.18.0+dfsg-1 | amd64,arm64,armhf,i386,ppc64el,s390x |
bookworm | 8.16.1+dfsg-1 | amd64,arm64,armhf,i386,ppc64el,s390x |
bullseye | 8.12.0-3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el |
buster | 8.9.0-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
jessie | 8.4pl4dfsg-1 | amd64,armel,armhf,i386 |
stretch | 8.6-4 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
upstream | 8.19.1 |
Debtags of package coq: |
devel | compiler |
field | mathematics |
interface | commandline, text-mode |
role | program |
scope | utility |
uitoolkit | ncurses |
|
License: DFSG free
|
Coq jest asystentem udowadniania nadrzędnej logiki, która pozwala na rozwój
programów komputerowych zgodnych z ich oficjalną specyfikacją. Został
opracowany przy użyciu Objective Caml i Camlp5.
Pakiet zawiera coqtop, interfejs wiersza poleceń do Coq.
Graficzny interfejs do Coq znajduje się w pakiecie coqide. Coq można
również stosować z ProofGeneral, który umożliwia edytowanie dowodów
przy użyciu emacs i xemacs. W tym celu należy zainstalować pakiet proofgeneral.
|
|
cvc3
Automatic theorem prover for SMT problems
|
Versions of package cvc3 |
Release | Version | Architectures |
stretch | 2.4.1-5.1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
jessie | 2.4.1-5 | amd64,armel,armhf,i386 |
Debtags of package cvc3: |
interface | commandline |
role | program |
|
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
automated theorem prover for SMT problems
|
Versions of package cvc4 |
Release | Version | Architectures |
bookworm | 1.8-3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
trixie | 1.8-3 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,s390x |
sid | 1.8-3 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
buster | 1.6-2 | amd64,i386,mips,mips64el,mipsel |
bullseye | 1.8-2 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
|
License: DFSG free
|
CVC4 is an efficient 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.
CVC4 is intended to be an open and extensible SMT engine, and it can
be used as a stand-alone tool or as a library. It is the fourth in
the Cooperating Validity Checker family of tools (also including CVC,
CVC Lite and CVC3). CVC4 has been designed to increase the
performance and reduce the memory overhead of its predecessors.
This package contains binaries needed to use CVC4 as a stand-alone
tool.
|
|
depqbf
solver for quantified boolean formulae
|
Versions of package depqbf |
Release | Version | Architectures |
jessie | 3.04-1 | amd64,armel,armhf,i386 |
stretch | 5.01-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
buster | 5.01-3 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
bullseye | 5.01-3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bookworm | 5.01-3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
trixie | 5.01-3 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,s390x |
sid | 5.01-3 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
|
License: DFSG free
|
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
Narzędzia uziemiające dla (rozłącznych) programów logicznych
|
Versions of package gringo |
Release | Version | Architectures |
sid | 5.6.2-1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
trixie | 5.6.2-1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,s390x |
bookworm | 5.4.1-3.1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bullseye | 5.4.1-3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
buster | 5.3.0-10 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
stretch | 5.1.0-4 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
jessie | 4.4.0-1 | amd64,armel,armhf,i386 |
upstream | 5.7.1 |
Debtags of package gringo: |
role | program |
|
License: DFSG free
|
Obecne rozwiązanie umożliwia solwerom pracę na programach uwolnionych
od zmiennych. Dlatego potrzebny jest program uziemiający, który na
podstawie programu wejściowego ze zmiennymi pierwszego rzędu obliczy
równoważny program uziemiający (bez zmiennych).
Ten pakiet zawiera następujące narzędzia:
- gringo: program uziemiający, który biorąc pod uwagę program wejściowy
ze zmiennymi pierwszego rzędu, oblicza równoważny program uziemiający
(wolny od zmiennych) w formacie aspif. Jego dane wyjściowe można
później przetworzyć za pomocą clasp, solwera "zestawu odpowiedzi"
(programowanie deklaratywne). Począwszy od piątej serii gringo, jego
dane wyjściowe nie są już bezpośrednio kompatybilne z solwerami,
takimi jak smodels lub cmodels odczytującymi format smodels. Aby
wykonać konwersję z formatu aspif do formatu smodels należy użyć
narzędzia lpconvert;
- clingo: łączy w sobie gringo i clasp w monolityczny system.
W ten sposób zapewnia większą kontrolę nad procesem uziemiania i
przetwarzania rozdzielczości, niż gringo i clasp mogą zapewnić
indywidualnie: powtarzalna rozdzielczość;
- lpconvert: konwerter pomiędzy formatami aspif gringo i smodels;
- reify: małe narzędzie reifikujące programy logiczne podane w
formacie aspif. Tworzy zestaw elementów, który można poddać
dalszej obróbce za pomocą gringo.
|
|
hol-light
|
Versions of package hol-light |
Release | Version | Architectures |
sid | 20231021-1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
jessie | 20131026-1 | amd64,armel,armhf,i386 |
stretch | 20170109-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
bullseye | 20190729-4 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bookworm | 20230128-1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
trixie | 20231021-1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,s390x |
|
License: DFSG free
|
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, system image
|
Versions of package hol88 |
Release | Version | Architectures |
buster | 2.02.19940316-35 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
jessie | 2.02.19940316-28 | amd64,armel,armhf,i386 |
sid | 2.02.19940316dfsg-5 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
trixie | 2.02.19940316dfsg-5 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,s390x |
bookworm | 2.02.19940316dfsg-5 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bullseye | 2.02.19940316-35.1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
stretch | 2.02.19940316-33 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
Debtags of package hol88: |
uitoolkit | ncurses |
|
License: DFSG free
|
The HOL System is an environment for interactive theorem proving in a
higher-order logic. Its most outstanding feature is its high degree
of programmability through the meta-language ML. The system has a
wide variety of uses from formalizing pure mathematics to
verification of industrial hardware. Academic and industrial sites
world-wide are using HOL.
|
|
lbt
converts from LTL formulas to Büchi automata
|
Versions of package lbt |
Release | Version | Architectures |
sid | 1.2.2-7 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
jessie | 1.2.2-5 | amd64,armel,armhf,i386 |
stretch | 1.2.2-6 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
buster | 1.2.2-6 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
bullseye | 1.2.2-7 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bookworm | 1.2.2-7 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
trixie | 1.2.2-7 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,s390x |
Debtags of package lbt: |
field | mathematics |
interface | commandline |
role | program |
scope | utility |
use | converting |
|
License: DFSG free
|
This software converts a linear temporal logic (ltl) formula to a
generalised Büchi automaton. The resulting automaton may be used, for
instance, in model checking, where it represents a property to be
verified from a model (e.g. a Petri net).
|
|
mace2
program that searches for finite models of first-order statements
|
Versions of package mace2 |
Release | Version | Architectures |
jessie | 3.3f-1.1 | amd64,armel,armhf,i386 |
Debtags of package mace2: |
role | program |
use | searching |
|
License: DFSG free
|
MACE is a program that searches for finite models of first-order and
equational statements developed at Argonne National Laboratory.
This package includes ANLDP, which calls the propositional decision
procedure at the core of MACE directly.
MACE serves as a complementary companion to OTTER, which
searches for refutations of the same class of statement. In
particular, if you have a first-order conjecture, OTTER will search
for a proof, and MACE will search for a counterexample from the same
input file.
|
|
maria
reachability analyzer for Algebraic System Nets
|
Versions of package maria |
Release | Version | Architectures |
buster | 1.3.5-4.1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
bookworm | 1.3.5-4.1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
jessie | 1.3.5-4 | amd64,armel,armhf,i386 |
stretch | 1.3.5-4.1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
sid | 1.3.5-4.2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
trixie | 1.3.5-4.2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,s390x |
bullseye | 1.3.5-4.1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
Debtags of package maria: |
devel | testing-qa |
field | mathematics |
interface | text-mode |
role | program |
scope | utility |
uitoolkit | ncurses |
|
License: DFSG free
|
Maria is a powerful tool designed to aid engineers in modelling and
solving concurrency related problems in parallel and distributed
computing systems.
Maria finds deadlocks and violations against safety or liveness
requirements by exploring all states that can be reached from the
initial state of a system. The tool manages tens or hundreds of
millions of reachable states and enabled actions.
The expressive power of Maria's formalism is close to high-level
programming languages, thanks to its rich data type system and
powerful algebraic operations.
|
|
matita
Interaktywne udowodnianie twierdzeń
|
Versions of package matita |
Release | Version | Architectures |
jessie | 0.99.1-3 | amd64,armel,armhf,i386 |
stretch | 0.99.3-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
Debtags of package matita: |
field | mathematics |
interface | commandline, x11 |
role | program |
uitoolkit | gtk |
use | checking |
x11 | application |
|
License: DFSG free
|
Matita jest graficznym programem służącym do udowodniania twierdzeń,
opartym na rachunku konstrukcji indukcyjnych (ang. Calculus of
(Co)Inductive Constructions).
|
|
maude
high-performance logical framework
|
Versions of package maude |
Release | Version | Architectures |
trixie | 3.2-2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,s390x |
sid | 3.2-2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
jessie | 2.6-6 | amd64,armel,armhf,i386 |
buster | 2.7-2 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
stretch | 2.7-2 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
bullseye | 3.1-2 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bookworm | 3.2-2 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
Debtags of package maude: |
uitoolkit | ncurses |
|
License: DFSG free
|
Maude is a high-performance reflective language and system supporting
both equational and rewriting logic specification and programming for
a wide range of applications. Maude has been influenced in important
ways by the OBJ3 language, which can be regarded as an equational
logic sublanguage. Besides supporting equational specification and
programming, Maude also supports rewriting logic computation.
Rewriting logic is a logic of concurrent change that can naturally
deal with state and with concurrent computations. It has good
properties as a general semantic framework for giving executable
semantics to a wide range of languages and models of concurrency. In
particular, it supports very well concurrent object-oriented
computation. The same reasons making rewriting logic a good semantic
framework make it also a good logical framework, that is, a metalogic
in which many other logics can be naturally represented and executed.
Maude supports in a systematic and efficient way logical
reflection. This makes Maude remarkably extensible and powerful,
supports an extensible algebra of module composition operations, and
allows many advanced metaprogramming and metalanguage
applications. Indeed, some of the most interesting applications of
Maude are metalanguage applications, in which Maude is used to create
executable environments for different logics, theorem provers,
languages, and models of computation.
Maude is of interest to the biomedical community for modeling and
analysis of biological systems.
|
|
minisat+
solver for pseudo-Boolean constraints
|
Versions of package minisat+ |
Release | Version | Architectures |
jessie | 1.0-2 | amd64,armel,armhf,i386 |
buster | 1.0-4 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
bullseye | 1.0-4 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bookworm | 1.0-4 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
trixie | 1.0-4 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,s390x |
sid | 1.0-4 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
stretch | 1.0-3 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
Debtags of package minisat+: |
field | mathematics |
role | program |
|
License: DFSG free
|
MinSat+ is a solver for Pseudo-Boolean Optimization (AKA 0-1
integer programming) that is based on the MiniSat SAT-solver. It
supports optimizing a linear objective function, subject to a set
of linear constraints. The variables of the objective function
and constraints are boolean, i.e. required to be 0 or
1. Pseudo-Boolean optimization can be used to solve many kinds of
combinatorial optimization problems. This version of Minisat+ is
compiled with bignum support for constraint coefficients.
|
|
mona
Narzędzie do udowadniania twierdzeń oparte na automatach
|
Versions of package mona |
Release | Version | Architectures |
stretch | 1.4-17-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
buster | 1.4-17-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
jessie | 1.4-15-1 | amd64,armel,armhf,i386 |
bullseye | 1.4-17-2 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bookworm | 1.4-18-1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
trixie | 1.4-18-1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,s390x |
sid | 1.4-18-1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
Debtags of package mona: |
field | mathematics |
role | program |
scope | utility |
|
License: DFSG free
|
MONA to narzędzie, które tłumaczy formuły w logice WS1S lub WS2S
na automaty skończone reprezentowane przez BDD. Formuły mogą wyrażać
wzorce wyszukiwania, właściwości czasowe układów reaktywnych, analizować
ograniczenia drzewa itp. MONA analizuje również automat powstały w wyniku
kompilacji i określa, czy formuła jest poprawna, a jeśli taka nie jest,
generuje kontrprzykład.
Dokumentacja jest dostępna na stronie internetowej MONA:
http://www.brics.dk/mona/.
|
|
picosat
SAT solver with proof and core support
|
Versions of package picosat |
Release | Version | Architectures |
stretch | 960-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
jessie | 960-1 | amd64,armel,armhf,i386 |
buster | 960-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
bullseye | 965-2 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bookworm | 965-2 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
trixie | 965-2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,s390x |
sid | 965-2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
Debtags of package picosat: |
field | mathematics |
role | program |
|
License: DFSG free
|
Despite the NP completeness of the satisfiabilty problem of Boolean formulas
(SAT), SAT solvers are often able to decide this problem in a reasonable time
frame. As all other NP complete problems are reducible to SAT, the solvers
have become a general purpose tool for this class of problems.
PicoSAT is a SAT solver that turned out to be faster on industrial instances
than MiniSAT 2.0 and also can generate proofs and cores in memory.
|
|
proofgeneral
Ogólny interfejs dla asystentów dowodzenia twierdzeń
|
Versions of package proofgeneral |
Release | Version | Architectures |
bookworm | 4.4.1~pre170114-1.2 | all |
stretch | 4.4.1~pre170114-1 | all |
jessie | 4.3~pre131011-0.2 | all |
trixie | 4.5-1 | all |
sid | 4.5-1 | all |
bullseye | 4.4.1~pre170114-1.2 | all |
Debtags of package proofgeneral: |
field | mathematics |
interface | text-mode, x11 |
role | plugin |
suite | emacs |
use | editing |
|
License: DFSG free
|
Proof General jest głównym trybem przekształcania Emacsa w interaktywny
system dowodzenia twierdzeń, który służy do pisania formalnych dowodów
matematycznych przy użyciu różnych narzędzi asystujących użytkownikowi przy
przeprowadzaniu dowodu.
Ten pakiet zapewnia wsparcie Proof General dla Coq (brak innego systemu
dowodzenia twierdzeń, który mógłby zapewniać odpowiednie wsparcie).
|
|
prover9
theorem prover and countermodel generator
|
Versions of package prover9 |
Release | Version | Architectures |
stretch | 0.0.200911a-2.1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
buster | 0.0.200911a-2.1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
jessie | 0.0.200911a-2.1 | amd64,armel,armhf,i386 |
|
License: DFSG free
|
This package provides the Prover9 resolution/paramodulation theorem
prover and the Mace4 countermodel generator.
Prover9 is an automated theorem prover for first-order and equational
logic. It is a successor of the Otter prover. Prover9 uses the
inference techniques of ordered resolution and paramodulation with
literal selection.
The program Mace4 searches for finite structures satisfying first-order
and equational statements, the same kind of statement that Prover9
accepts. If the statement is the denial of some conjecture, any
structures found by Mace4 are counterexamples to the conjecture.
Mace4 can be a valuable complement to Prover9, looking for
counterexamples before (or at the same time as) using Prover9 to search
for a proof. It can also be used to help debug input clauses and formulas
for Prover9.
|
|
sat4j
Wydajna biblioteka solverów SAT w Javie
|
Versions of package sat4j |
Release | Version | Architectures |
trixie | 2.3.5-0.3 | all |
bookworm | 2.3.5-0.3 | all |
bullseye | 2.3.5-0.3 | all |
buster | 2.3.5-0.3 | all |
jessie | 2.3.3-1 | all |
stretch | 2.3.5-0.2 | all |
sid | 2.3.5-0.3 | all |
Debtags of package sat4j: |
field | mathematics |
role | program, shared-lib |
|
License: DFSG free
|
Celem biblioteki SAT4J jest zapewnienie wydajnej biblioteki solverów SAT w Javie. W porównaniu z projektem OpenSAT biblioteka SAT4J jest skierowana do pierwszych użytkowników "czarnych skrzynek" SAT, którzy chcą osadzić technologie SAT w swoich aplikacjach, nie martwiąc się o szczegóły. Ponadto, autorzy projektu SAT4J próbują zapewnić podstawowe zaplecze pracy naukowcom SAT.
|
|
spass
automated theorem prover for first-order logic with equality
|
Versions of package spass |
Release | Version | Architectures |
stretch | 3.7-4 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
sid | 3.9-1.1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
trixie | 3.9-1.1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,s390x |
bookworm | 3.9-1.1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bullseye | 3.9-1.1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
jessie | 3.7-3 | amd64,armel,armhf,i386 |
Debtags of package spass: |
field | mathematics |
|
License: DFSG free
|
SPASS is a saturation-based automated theorem prover for first-order logic with
equality. It is unique due to the combination of the superposition calculus
with specific inference/reduction rules for sorts (types) and a splitting rule
for case analysis motivated by the beta-rule of analytic tableaux and the case
analysis employed in the Davis-Putnam procedure. Furthermore, SPASS provides a
sophisticated clause normal form translation.
This package consists of the SPASS/FLOTTER binary, documentation, and a small
example collection. The tools collections contain the proof checker pcs, the
syntax translators dfg2otter and dfg2tptp, and the ASCII pretty printer
dfg2ascii.
|
|
toulbar2
Exact combinatorial optimization for Graphical Models
|
Versions of package toulbar2 |
Release | Version | Architectures |
sid | 1.2.1+dfsg-0.1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
buster | 1.0.0+dfsg3-2 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
bullseye | 1.1.1+dfsg-1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bookworm | 1.1.1+dfsg-1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
trixie | 1.2.1+dfsg-0.1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,s390x |
|
License: DFSG free
|
Toulbar2 is an exact discrete optimization tool for Graphical Models
such as Cost Function Networks, Markov Random Fields, Weighted Constraint
Satisfaction Problems and Bayesian Nets.
|
|
why
Software verification tool
|
Versions of package why |
Release | Version | Architectures |
jessie | 2.34-2 | amd64,armel,armhf,i386 |
Debtags of package why: |
devel | testing-qa |
role | program |
|
License: DFSG free
|
Why aims at being a verification conditions generator (VCG) back-end
for other verification tools. It provides a powerful input language
including higher-order functions, polymorphism, references, arrays and
exceptions. It generates proof obligations for many systems: the proof
assistants Coq, PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar and the
decision procedures Simplify, Alt-Ergo, Yices, CVC Lite and haRVey.
|
|
why3
Software verification platform
|
Versions of package why3 |
Release | Version | Architectures |
sid | 1.6.0-1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
buster | 1.2.0-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
bullseye | 1.3.3-1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
stretch | 0.87.3-2 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
bookworm | 1.5.1-1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
trixie | 1.6.0-1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,s390x |
upstream | 1.7.1 |
|
License: DFSG free
|
Why3 is a platform for deductive program verification. It provides a
rich language for specification and programming, called WhyML, and
relies on external theorem provers, both automated and interactive,
to discharge verification conditions. Why3 comes with a standard
library of logical theories (integer and real arithmetic, Boolean
operations, sets and maps, etc.) and basic programming data
structures (arrays, queues, hash tables, etc.). A user can write
WhyML programs directly and get correct-by-construction OCaml
programs through an automated extraction mechanism. WhyML is also
used as an intermediate language for the verification of C, Java, or
Ada programs.
Why3 is a complete reimplementation of the former Why platform. Among
the new features are: numerous extensions to the input language, a
new architecture for calling external provers, and a well-designed
API, allowing to use Why3 as a software library. An important
emphasis is put on modularity and genericity, giving the end user a
possibility to easily reuse Why3 formalizations or to add support for
a new external prover if wanted.
|
|
z3
theorem prover from Microsoft Research
|
Versions of package z3 |
Release | Version | Architectures |
trixie | 4.8.12-3.1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,s390x |
stretch | 4.4.1-1~deb9u1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
buster | 4.4.1-1~deb10u1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
bullseye | 4.8.10-1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bookworm | 4.8.12-3.1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
sid | 4.8.12-3.1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
upstream | 4.13.0 |
|
License: DFSG free
|
Z3 is a state-of-the-art theorem prover from Microsoft Research. It can be
used to check the satisfiability of logical formulas over one or more
theories. Z3 offers a compelling match for software analysis and verification
tools, since several common software constructs map directly into supported
theories.
The Z3 input format is an extension of the one defined by the SMT-LIB 2.0
standard.
|
|
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 |
Release | Version | Architectures |
stretch | 1.7.6+dfsg1-2 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
experimental | 1.8.4+dfsg-1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
sid | 1.8.3-3 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
trixie | 1.8.3-3 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,s390x |
bookworm | 1.8.3-3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bullseye | 1.8.3-3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
buster | 1.8.3-2 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
jessie | 1.7.6+dfsg1-1 | amd64,armel,armhf,i386 |
|
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.
|
|
|