Debian Science Project
Summary
Logic
Debian Science Logic packages

This metapackage is part of the Debian Pure Blend "Debian Science" and installs packages related to Computational Logic. It contains formula transformation tools, solvers for formulas specified in various logics, interactive proof systems, etc.

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
ReleaseVersionArchitectures
bullseye2.5.4.1-3all
sid2.5.4.1-3all
wheezy2.3.0.1-2all
jessie2.4.0.2-2all
stretch2.5.1.1-3all
buster2.5.4.1-3all
upstream2.6.0.1
Debtags of package agda:
rolemetapackage
Popcon: 0 users (0 upd.)*
Newer upstream!
License: DFSG free
Git

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
프로그램 검증에 사용되는 자동화된 정리 증명계
Versions of package alt-ergo
ReleaseVersionArchitectures
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-4amd64,arm64,armel,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye2.0.0-4amd64,arm64,armel,i386,mips,mips64el,mipsel,ppc64el,s390x
buster2.0.0-3amd64,arm64,armel,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch1.30-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Debtags of package alt-ergo:
roleprogram
uitoolkitgtk
Popcon: 4 users (15 upd.)*
Versions and Archs
License: DFSG free
Git

Alt-Ergo는 프로그램 검증에 있어 어플리케이션을 대상으로 하는 자동화된 정리 증명계입니다. 등가 이론 X 에 의해 매개변수화 된 합동 폐쇄 알고리즘인, CC(X) 에 기반합니다. Alt-Ergo는 명제 로직, 선형 산술, 해석되지 않는 함수 기호, 연 관 교환 가능 함수 기호, 다형 배열, 사용자 정의 다형 레코드, 다형성 열거 유 형이 내장된 증명계입니다. 임의 사용자 정의 대수 유형, 1차 수량 한정자, 비선 형 산술에 대한 추론이 제한되어 있습니다.

이 패키지는 명령행 실행 및 그래픽 인터페이스로서 증명계를 포함합니다.

Boolector
SMT solver for bit-vectors and arrays
Maintainer: Michael Tautschnig
Versions of package boolector
ReleaseVersionArchitectures
jessie1.5.118.6b56be4.121013-1amd64,armel,armhf,i386
bullseye1.5.118.6b56be4.121013-1amd64,arm64,armel,armhf,i386,mips,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
sid1.5.118.6b56be4.121013-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
wheezy1.4.ffc2089.100608-1amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
squeeze1.4.ffc2089.100608-1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
Debtags of package boolector:
roleprogram
Popcon: 2 users (3 upd.)*
Versions and Archs
License: DFSG free

Boolector is an efficient SMT solver for the quantifier-free theory of bit-vectors in combination with the quantifier-free extensional theory of arrays.

Clasp
갈등 주도 nogood 학습 해결 세트 솔버
Versions of package clasp
ReleaseVersionArchitectures
sid3.3.4-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
wheezy2.0.6-2amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie3.1.0-1amd64,armel,armhf,i386
stretch3.2.1-3amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster3.3.4-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye3.3.4-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Debtags of package clasp:
roleprogram
Popcon: 84 users (292 upd.)*
Versions and Archs
License: DFSG free
Git

clasp는 (확장된) 일반 논리 프로그램을 위한 해답 집합 솔버입니다. answer set programming(ASP)의 고급 모델링 기능과 부울 제약 해결 영역의 최첨단 기술을 결합합니다. 주 clasp 알고리즘은 적합성 검사(SAT)에서 매우 성공적이었던 기 술, 충돌 기반 nogood 학습에 의존합니다. 다른 학습 ASP 솔버와 달리, clasp는 SAT 솔버 또는 다른 기존의 ASP 솔버같은 레거시 소프트웨어에 의존하지 않습니 다. 오히려, clasp는 충돌 기반 nogood 학습을 기반으로 해결 세트 솔버를 위해 진정으로 개발되었습니다. clasp는 ASP 솔버 (LPARSE 출력 형식), SAT 솔버 (단 순 DIMACS/CNF 형식) 또는 PB 솔버 (OPB 형식)로 적용할 수 있습니다.

Coala
translates action languages into answer set programs
Versions of package coala
ReleaseVersionArchitectures
wheezy1.0.1-5amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie1.0.1-5amd64,armel,armhf,i386
Debtags of package coala:
roleprogram
Popcon: 0 users (0 upd.)*
Versions and Archs
License: DFSG free
Git

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
ReleaseVersionArchitectures
stretch2.8.12-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
sid2.9.9+repack1-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye2.9.9+repack1-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster2.9.9+repack1-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie2.8.12-1amd64,armel,armhf,i386
upstream2.10.3
Popcon: 27 users (275 upd.)*
Newer upstream!
License: DFSG free
Git

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
ReleaseVersionArchitectures
sid5.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
buster5.6.16+repack1-1.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye5.6.16+repack1-1.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
upstream5.6.17
Popcon: 15 users (19 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
proof assistant for higher-order logic (toplevel and compiler)
Versions of package coq
ReleaseVersionArchitectures
bullseye8.9.0-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
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
stretch8.6-4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster8.9.0-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
sid8.9.0-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
squeeze8.2.pl2+dfsg-1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
upstream8.9.1
Debtags of package coq:
develcompiler
fieldmathematics
interfacecommandline, text-mode
roleprogram
scopeutility
uitoolkitncurses
Popcon: 32 users (71 upd.)*
Newer upstream!
License: DFSG free
Git

Coq is a proof assistant for higher-order logic, which allows the development of computer programs consistent with their formal specification. It is developed using Objective Caml and Camlp5.

This package provides coqtop, a command line interface to Coq.

The proofgeneral package allows proofs to be edited using Emacs and XEmacs.

The package is enhanced by the following packages: libaac-tactics-ocaml libssreflect-ocaml
Cvc3
SMT 문제를 위한 자동 정리 프루버
Maintainer: Morgan Deters (Adrian Bunk)
Versions of package cvc3
ReleaseVersionArchitectures
sid2.4.1-5.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch2.4.1-5.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie2.4.1-5amd64,armel,armhf,i386
wheezy2.4.1-4amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
squeeze2.2-13amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
Debtags of package cvc3:
interfacecommandline
roleprogram
Popcon: 1 users (1 upd.)*
Versions and Archs
License: DFSG free

CVC3은 충족성 모듈 이론(SMT) 문제에 대한 자동 정리 프루버입니다. 다수의 내 장된 논리 이론 및 그 조합에서 일차 공식의 타당성 (또는 이중성, 만족성)을 입 증하는데 사용할 수 있습니다.

CVC3는 스탠포드 대학에서 SVC 시스템으로 시작된, 인기있는 일련의 SMT 프루버 의 마지막 성과물입니다. 특히 전버전인 CVS Lite의 코드를 기반으로 만들었습니 다. 고수준 디자인은 Sammy 프루버의 디자인을 따릅니다.

CVC3은 다형성 타입을 갖는 1차 로직 버젼과 함께 작동하며 e아므과 같은 다양한 기능을 포함합니다:

  • 몇몇 내장 기본 이론: 유리수 및 정수 선형 산술, 배열, 튜플, 레코드, 유도 데이타 유형, 비트 벡터, 해석되지 않는 함수 기호에 대한 등식;
  • 한정사 지원;
  • 대화형 텍스트 기반 인터페이스;
  • 다른 시스템에 임베이드되는 풍부한 C, C++, JAVA API들
  • 증명 및 모델 생성 기능;
  • 술어 서브타입;
  • 본질적으로 연구 또는 상업적 사용에 대해 제한이없음 (라이센스 참조).

이 패키지는 CVC3 명령행 프로그램을 포함합니다.

The package is enhanced by the following packages: cvc3-el
Cvc4
automated theorem prover for SMT problems
Versions of package cvc4
ReleaseVersionArchitectures
bullseye1.6-2amd64,i386,mips,mips64el,mipsel
buster1.6-2amd64,i386,mips,mips64el,mipsel
sid1.6-2amd64,i386,mips,mips64el,mipsel
Popcon: 3 users (16 upd.)*
Versions and Archs
License: DFSG free
Git

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
ReleaseVersionArchitectures
buster5.01-3amd64,arm64,armel,armhf,i386,mips,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
sid5.01-3amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch5.01-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye5.01-3amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
upstream6.03
Popcon: 5 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
(선언적) 논리 프로그램용 그라운딩 도구
Versions of package gringo
ReleaseVersionArchitectures
sid5.3.0-10amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye5.3.0-10amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
wheezy3.0.4-3amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
stretch5.1.0-4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie4.4.0-1amd64,armel,armhf,i386
buster5.3.0-10amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Debtags of package gringo:
roleprogram
Popcon: 88 users (293 upd.)*
Versions and Archs
License: DFSG free
Git

현재 응답 집합 해결 프로그램은 가변 변수 프로그램에서 작동합니다. 따라서 일 차 변수를 가지는 입력 프로그램이 주어지면 동등한 그라운드 (비가변) 프로그램 을 계산할 그라운더가 필요해집니다.

이 패키지는 아래 도구들을 포함합니다:

  • gringo:일차 변수를 가지는 입력 프로그램이 주어지면, aspif 형식에서 동등한 그라운드 (비가변) 프로그램을 계산하는 그라운더. 출력은 응답 집합 해결 프로그램 clasp를 통해 추가로 처리할 수 있습니다. gringo 시리즈 5부터는 smodels 형식을 읽을 수 있는 smodels 또는 cmodels 같은 해결 프로그램과 출력에 있어 더 이상 직접 호환을 제공하지 않습니다. aspif 형식을 smodels 형식으로 변환하기 위해서는 lpconvert를 사용하십시오.
  • clingo: gringo 와 clasp를 모놀로틱 시스템에 결합합니다. 이 방법은 gringo 및 clasp가 단독으로 제공할 수 있는 것 보다 그라운딩 및 해결 프로세스에 대한 더 많은 제어를 제공합니다: multi-shot solving.
  • lpconvert: gringo의 aspif 및 smodels 형식간 변환기.
  • reify: aspif 형식으로 제공된 논리 프로그램을 구체화하는 작은 유틸리티. 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,mips,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
bullseye20190729-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Popcon: 3 users (3 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, system image
Maintainer: Camm Maguire
Versions of package hol88
ReleaseVersionArchitectures
jessie2.02.19940316-28amd64,armel,armhf,i386
sid2.02.19940316-35amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch2.02.19940316-33amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
wheezy2.02.19940316-15amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
squeeze2.02.19940316-13.1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
buster2.02.19940316-35amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye2.02.19940316-35amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Debtags of package hol88:
uitoolkitncurses
Popcon: 1 users (8 upd.)*
Versions and Archs
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
LTL 공식을 Büchi 오토마타로 변환
Versions of package lbt
ReleaseVersionArchitectures
sid1.2.2-6amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
squeeze1.2.2-4amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy1.2.2-5amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,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,mips,mips64el,mipsel,ppc64el,s390x
Debtags of package lbt:
fieldmathematics
interfacecommandline
roleprogram
scopeutility
useconverting
Popcon: 8 users (6 upd.)*
Versions and Archs
License: DFSG free
Git

이 소프트웨어는 LTL(linear temporal logic) 공식을 일반화된 Büchi 오토마톤으로 변환합니다. 결과로 나온 오토마톤은 예를 들어 모델 점검, 즉 모델(예: Petri net)에서 검증해야 할 특성을 나타내는 데 쓰입니다.

Mace2
program that searches for finite models of first-order statements
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 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
ReleaseVersionArchitectures
sid1.3.5-4.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye1.3.5-4.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster1.3.5-4.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch1.3.5-4.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie1.3.5-4amd64,armel,armhf,i386
wheezy1.3.5-4amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
squeeze1.3.5-2amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
Debtags of package maria:
develtesting-qa
fieldmathematics
interfacetext-mode
roleprogram
scopeutility
uitoolkitncurses
Popcon: 10 users (18 upd.)*
Versions and Archs
License: DFSG free
Git

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
interactive theorem prover
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,mips,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 (3 upd.)*
Versions and Archs
License: DFSG free
Git

Matita is a graphical interactive theorem prover based on the Calculus of (Co)Inductive Constructions.

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

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.

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+
solver for pseudo-Boolean constraints
Versions of package minisat+
ReleaseVersionArchitectures
stretch1.0-3amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
sid1.0-4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye1.0-4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster1.0-4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
wheezy1.0-2amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie1.0-2amd64,armel,armhf,i386
Debtags of package minisat+:
fieldmathematics
roleprogram
Popcon: 3 users (4 upd.)*
Versions and Archs
License: DFSG free
Git

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
theorem prover based on automata
Versions of package mona
ReleaseVersionArchitectures
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
squeeze1.4-13-1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
sid1.4-17-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye1.4-17-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Debtags of package mona:
fieldmathematics
roleprogram
scopeutility
Popcon: 3 users (8 upd.)*
Versions and Archs
License: DFSG free
Git

MONA is a tool that translates formulas in the logics WS1S or WS2S into finite-state automata represented by BDDs. The formulas may express search patterns, temporal properties of reactive systems, parse tree constraints, etc. MONA also analyses the automaton resulting from the compilation, and determines whether the formula is valid and, if the formula is not valid, generates a counter-example.

Documentation is available from the MONA website http://www.brics.dk/mona/.

Picosat
SAT solver with proof and core support
Maintainer: Michael Tautschnig
Versions of package picosat
ReleaseVersionArchitectures
jessie960-1amd64,armel,armhf,i386
squeeze913-4amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
sid960-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye960-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster960-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch960-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
wheezy936-4amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
upstream965
Debtags of package picosat:
fieldmathematics
roleprogram
Popcon: 6 users (1 upd.)*
Newer upstream!
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.

Screenshots of package picosat
Proofgeneral
generic frontend for proof assistants
Versions of package proofgeneral
ReleaseVersionArchitectures
stretch4.4.1~pre170114-1all
squeeze3.7-4all
bullseye4.4.1~pre170114-1.1all
wheezy4.2~pre120605-2all
jessie4.3~pre131011-0.2all
sid4.4.1~pre170114-1.1all
Debtags of package proofgeneral:
fieldmathematics
interfacetext-mode, x11
roleplugin
suiteemacs
useediting
Popcon: 24 users (16 upd.)*
Versions and Archs
License: DFSG free

Proof General is a major mode to turn Emacs into an interactive proof assistant to write formal mathematical proofs using a variety of theorem provers.

This package provides Proof General support for Coq. (There is no other proof assistant that one could sensibly support.)

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
theorem prover and countermodel generator
Versions of package prover9
ReleaseVersionArchitectures
bullseye0.0.200911a-2.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
squeeze0.0.200902a-2amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy0.0.200902a-2.1amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,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
sid0.0.200911a-2.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Popcon: 31 users (16 upd.)*
Versions and Archs
License: DFSG free
Bzr

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
자바에서 SAT 솔버에 대한 효율적인 라이브러리
Versions of package sat4j
ReleaseVersionArchitectures
bullseye2.3.5-0.3all
sid2.3.5-0.3all
buster2.3.5-0.3all
stretch2.3.5-0.2all
jessie2.3.3-1all
squeeze2.2.0-3all
wheezy2.3.1-1all
Debtags of package sat4j:
fieldmathematics
roleprogram, shared-lib
Popcon: 244 users (97 upd.)*
Versions and Archs
License: DFSG free

SAT4J의 목적은 자바에서 SAT 솔버에 대한 효과적인 라이브러리를 제공하는 것 입니다. OpenSAT 프로젝트와 비교해서, SAT4J 라이브러리는 세부 사항에 대한 걱 정 없이 어플리케이션에 SAT 기술을 포함하고자 하는 SAT "블랙 박스" 첫 사용자 를 대상으로 합니다. SAT4J 프로젝트는 또한 SAT 연구원들을 위한 작업의 기초를 제공하려 노력합니다.

Spass
automated theorem prover for first-order logic with equality
Versions of package spass
ReleaseVersionArchitectures
jessie3.7-3amd64,armel,armhf,i386
sid3.7-4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
wheezy3.7-3amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
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
Debtags of package spass:
fieldmathematics
Popcon: 2 users (1 upd.)*
Versions and Archs
License: DFSG free
Git

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
ReleaseVersionArchitectures
buster1.0.0+dfsg3-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
sid1.0.0+dfsg3-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye1.0.0+dfsg3-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Popcon: 10 users (17 upd.)*
Versions and Archs
License: DFSG free
Git

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
ReleaseVersionArchitectures
wheezy2.30+dfsg-5amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
squeeze2.26+dfsg-2+squeeze1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
jessie2.34-2amd64,armel,armhf,i386
Debtags of package why:
develtesting-qa
roleprogram
Popcon: 1 users (0 upd.)*
Versions and Archs
License: DFSG free
Git

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.

Screenshots of package why
Why3
Software verification platform
Versions of package why3
ReleaseVersionArchitectures
stretch0.87.3-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
sid1.2.0-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye1.2.0-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster1.2.0-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Popcon: 2 users (12 upd.)*
Versions and Archs
License: DFSG free
Git

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
ReleaseVersionArchitectures
stretch4.4.1-0.4~deb9u1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster4.4.1-0.4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye4.4.1-0.4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
sid4.4.1-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
upstream4.8.4
Popcon: 14 users (16 upd.)*
Newer upstream!
License: DFSG free
Git

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
ReleaseVersionArchitectures
sid1.8.3-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie1.7.6+dfsg1-1amd64,armel,armhf,i386
stretch1.7.6+dfsg1-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster1.8.3-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye1.8.3-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Popcon: 4 users (9 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 196492