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
|
Versions of package agda |
Release | Version | Architectures |
trixie | 2.6.4.3-1 | all |
bookworm | 2.6.2.2-1.1 | all |
bullseye | 2.6.1-1 | all |
buster | 2.5.4.1-3 | all |
stretch | 2.5.1.1-3 | all |
sid | 2.6.4.3-1 | all |
jessie | 2.4.0.2-2 | all |
upstream | 2.7.0.1 |
Debtags of package agda: |
role | metapackage |
|
License: DFSG free
|
Agda는 종속 타입 함수형 프로그래밍 언어입니다: Haskell의 GADT처럼 귀납적인 관계를 가지고 있지만, 유형이 아닌 단지 값에 의해서 인덱스될 수 있습니다. 모듈, mixfix 연산자, 유니코드 문자, 대화형 Emacs 인터페이스등을 매개변수화 합니다 (형식 검사기는 개발에 도움을 줄 수 있습니다).
Agda는 증명 보조자이기도 합니다: 증명 작성 및 확인을 위한 대화형 시스템입니다. Agda는 직관주의적 유형 이론을 기반으로 하며, 이 이론은 스웨덴 논리학자 Per Martin-Löf 가 개발한 건설 수학을 위한 기본 시스템입니다. Coq, Epigram, NuPRL 같은 종속 유형을 기반으로 하는 다른 증명 보조자와 많이 유사합니다.
이 패키지는 Agda의 이맥스 모드, 실행 파일, 표준 라이브러리, 문서를 제공하는 메타 패키지입니다.
|
|
alt-ergo
Automatic theorem prover dedicated to program verification
|
Versions of package alt-ergo |
Release | Version | Architectures |
buster | 2.0.0-3 | amd64,arm64,i386 |
bullseye | 2.0.0-7 | amd64,arm64,armel,i386,mips64el,mipsel,ppc64el,s390x |
stretch | 1.30-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
jessie | 0.95.2-3 | amd64,armel,armhf,i386 |
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
|
Versions of package boolector |
Release | Version | Architectures |
stretch | 1.5.118.6b56be4.121013-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
jessie | 1.5.118.6b56be4.121013-1 | amd64,armel,armhf,i386 |
buster | 1.5.118.6b56be4.121013-1 | amd64,arm64,armhf,i386 |
bullseye | 1.5.118.6b56be4.121013-1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,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,riscv64,s390x |
sid | 1.5.118.6b56be4.121013-1.3 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
Debtags of package boolector: |
role | program |
|
License: DFSG free
|
Boolector는 어레이의 quantifier-free 확장 이론과 결합하여 비트 벡터의 quantifier-free 이론을 위한 효과적인 SMT 솔버입니다.
|
|
clasp
|
Versions of package clasp |
Release | Version | Architectures |
trixie | 3.3.5-4.2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
sid | 3.3.5-4.2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,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 |
buster | 3.3.4-2 | amd64,arm64,armhf,i386 |
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는 (확장된) 일반 논리 프로그램을 위한 해답 집합 솔버입니다. answer set
programming(ASP)의 고급 모델링 기능과 부울 제약 해결 영역의 최첨단 기술을
결합합니다. 주 clasp 알고리즘은 적합성 검사(SAT)에서 매우 성공적이었던 기
술, 충돌 기반 nogood 학습에 의존합니다. 다른 학습 ASP 솔버와 달리, clasp는
SAT 솔버 또는 다른 기존의 ASP 솔버같은 레거시 소프트웨어에 의존하지 않습니
다. 오히려, clasp는 충돌 기반 nogood 학습을 기반으로 해결 세트 솔버를 위해
진정으로 개발되었습니다. clasp는 ASP 솔버 (LPARSE 출력 형식), SAT 솔버 (단
순 DIMACS/CNF 형식) 또는 PB 솔버 (OPB 형식)로 적용할 수 있습니다.
|
|
coinor-cbc
Coin-or branch-and-cut mixed integer programming solver
|
Versions of package coinor-cbc |
Release | Version | Architectures |
bookworm | 2.10.8+ds1-1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bullseye | 2.10.5+ds1-3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
buster | 2.9.9+repack1-1 | amd64,arm64,armhf,i386 |
stretch | 2.8.12-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
jessie | 2.8.12-1 | amd64,armel,armhf,i386 |
sid | 2.10.12+ds-1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
trixie | 2.10.12+ds-1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,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 |
sid | 5.6.17+dfsg-1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
jessie | 5.6.1-1 | amd64,armel,armhf,i386 |
stretch | 5.6.1-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
buster | 5.6.16+repack1-1.1 | amd64,arm64,armhf,i386 |
bullseye | 5.6.16+repack1-3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bookworm | 5.6.17+dfsg-1 | amd64,arm64,armel,armhf,i386,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
proof assistant for higher-order logic (toplevel and compiler)
|
Versions of package coq |
Release | Version | Architectures |
sid | 8.20.0+dfsg-1 | amd64,arm64,ppc64el,riscv64,s390x |
jessie | 8.4pl4dfsg-1 | amd64,armel,armhf,i386 |
buster | 8.9.0-1 | amd64,arm64,armhf,i386 |
bullseye | 8.12.0-3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el |
stretch | 8.6-4 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
bookworm | 8.16.1+dfsg-1 | amd64,arm64,armhf,i386,ppc64el,s390x |
trixie | 8.20.0+dfsg-1 | amd64,arm64,ppc64el,riscv64,s390x |
Debtags of package coq: |
devel | compiler |
field | mathematics |
interface | commandline, text-mode |
role | program |
scope | utility |
uitoolkit | ncurses |
|
License: DFSG free
|
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.
A graphical interface for Coq is provided in the coqide package.
Coq can also be used with ProofGeneral, which allows proofs to be
edited using emacs and xemacs. This requires the proofgeneral
package to be installed.
|
|
cvc4
automated theorem prover for SMT problems
|
Versions of package cvc4 |
Release | Version | Architectures |
bullseye | 1.8-2 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
buster | 1.6-2 | amd64,i386 |
bookworm | 1.8-3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
trixie | 1.8-3 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
sid | 1.8-3 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,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 |
bookworm | 5.01-3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bullseye | 5.01-3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
buster | 5.01-3 | amd64,arm64,armhf,i386 |
stretch | 5.01-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
trixie | 5.01-3 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
jessie | 3.04-1 | amd64,armel,armhf,i386 |
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.
|
|
drat-trim
??? missing short description for package drat-trim :-(
|
Versions of package drat-trim |
Release | Version | Architectures |
trixie | 0.0~git20240428.effa1dc-2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
sid | 0.0~git20240428.effa1dc-2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
upstream | 0.0~git20241125.2e3b2dc |
|
License: DFSG free
|
|
|
gringo
|
Versions of package gringo |
Release | Version | Architectures |
jessie | 4.4.0-1 | amd64,armel,armhf,i386 |
stretch | 5.1.0-4 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
buster | 5.3.0-10 | amd64,arm64,armhf,i386 |
bullseye | 5.4.1-3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bookworm | 5.4.1-3.1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
sid | 5.6.2-2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
trixie | 5.6.2-2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
upstream | 5.7.1 |
Debtags of package gringo: |
role | program |
|
License: DFSG free
|
현재 응답 집합 해결 프로그램은 가변 변수 프로그램에서 작동합니다. 따라서 일
차 변수를 가지는 입력 프로그램이 주어지면 동등한 그라운드 (비가변) 프로그램
을 계산할 그라운더가 필요해집니다.
이 패키지는 아래 도구들을 포함합니다:
- 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로 더 처리할 수 있는 일련의 사실들을 만들어냅니다.
|
|
hol-light
|
Versions of package hol-light |
Release | Version | Architectures |
sid | 3.0.0-1 | amd64,arm64,ppc64el,riscv64,s390x |
sid | 20231021-2 | armel,armhf,i386,mips64el |
bookworm | 20230128-1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bullseye | 20190729-4 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
stretch | 20170109-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
jessie | 20131026-1 | amd64,armel,armhf,i386 |
|
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 |
jessie | 2.02.19940316-28 | amd64,armel,armhf,i386 |
trixie | 2.02.19940316dfsg-5 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,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 |
buster | 2.02.19940316-35 | amd64,arm64,armhf,i386 |
stretch | 2.02.19940316-33 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
sid | 2.02.19940316dfsg-5 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,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.
|
|
kissat
??? missing short description for package kissat :-(
|
Versions of package kissat |
Release | Version | Architectures |
trixie | 4.0.1-3 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
sid | 4.0.1-3 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
|
License: DFSG free
|
|
|
lbt
|
Versions of package lbt |
Release | Version | Architectures |
trixie | 1.2.2-7 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
sid | 1.2.2-7 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
bookworm | 1.2.2-7 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bullseye | 1.2.2-7 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
buster | 1.2.2-6 | amd64,arm64,armhf,i386 |
stretch | 1.2.2-6 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
jessie | 1.2.2-5 | amd64,armel,armhf,i386 |
Debtags of package lbt: |
field | mathematics |
interface | commandline |
role | program |
scope | utility |
use | converting |
|
License: DFSG free
|
이 소프트웨어는 LTL(linear temporal logic) 공식을 일반화된 Büchi 오토마톤으로
변환합니다. 결과로 나온 오토마톤은 예를 들어 모델 점검, 즉 모델(예: Petri
net)에서 검증해야 할 특성을 나타내는 데 쓰입니다.
|
|
maria
reachability analyzer for Algebraic System Nets
|
Versions of package maria |
Release | Version | Architectures |
jessie | 1.3.5-4 | amd64,armel,armhf,i386 |
trixie | 1.3.5-6 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
bookworm | 1.3.5-4.1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
sid | 1.3.5-6 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
buster | 1.3.5-4.1 | amd64,arm64,armhf,i386 |
bullseye | 1.3.5-4.1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
stretch | 1.3.5-4.1 | amd64,arm64,armel,armhf,i386,mips,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.
|
|
maude
|
Versions of package maude |
Release | Version | Architectures |
jessie | 2.6-6 | amd64,armel,armhf,i386 |
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 |
trixie | 3.4-1 | amd64,arm64,mips64el,ppc64el,riscv64,s390x |
sid | 3.4-1 | amd64,arm64,mips64el,ppc64el,riscv64,s390x |
buster | 2.7-2 | amd64,arm64,armhf,i386 |
upstream | 3.5 |
Debtags of package maude: |
uitoolkit | ncurses |
|
License: DFSG free
|
Maude는 광범위한 어플리케이션을 위한 방정식 및 재작성 로직 사양과 프로그래밍을 모두 지원하는 고성능 반사 언어 및 시스템입니다. Maude는 방정식 논리 하위 언어로 간주될 수 있는 OBJ3 언어의 영향을 크게 받았습니다. 방정식 사양과 프로그래밍 지원 외에도 Maude는 논리 계산 재작성도 지원합니다.
로직을 재작성하는 것은 상태와 동시 계산을 자연스럽게 처리할 수 있는 동시 변경 논리입니다. 이는 광범위한 언어 및 동시성 모델에 실행 가능한 의미 체계를 제공하기 위한 일반적인 의미 체계 프레임워크로서 좋은 특성을 가지고 있습니다. 특히 동시 객체 지향 계산을 매우 잘 지원합니다. 로직 재작성을 좋은 의미론적 프레임워크로 만드는 동일한 이유로 인해 이를 좋은 논리적 프레임워크, 즉 다른 많은 로직이 자연스럽게 표현되고 실행될 수 있는 메타로직으로 만듭니다.
Maude는 체계적이고 효율적인 방식으로 논리적 성찰을 지원합니다. 이는 Maude를 놀랍도록 확장 가능하고 강력하게 만들고, 모듈 구성 작업의 확장 가능한 대수학을 지원하며, 많은 고급 메타 프로그래밍 및 메타 언어 어플리케이션을 가능하게 합니다. 실제로 Maude의 가장 흥미로운 어플리케이션중 일부는 메타언어 어플리케이션입니다. 여기서 Maude는 다양한 논리, 정리 프로버, 언어 및 계산 모델에 대한 실행 가능한 환경을 만드는 데 사용됩니다.
Maude는 생물학적 시스템의 모델링 및 분석에 대한 생의학 커뮤니티의 관심을 끌고 있습니다.
|
|
minisat+
|
Versions of package minisat+ |
Release | Version | Architectures |
trixie | 1.0-5 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
sid | 1.0-5 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
jessie | 1.0-2 | amd64,armel,armhf,i386 |
stretch | 1.0-3 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
buster | 1.0-4 | amd64,arm64,armhf,i386 |
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 |
Debtags of package minisat+: |
field | mathematics |
role | program |
|
License: DFSG free
|
MinSat+는 MiniSat SAT-solver를 기반으로 하는 Pseudo-Boolean Optimization (AKA 0-1 정수 프로그래밍)을 위한 솔버입니다. 일련의 선형 제약 조건에 따라 선형 목적 함수 최적화를 지원합니다. 목적 함수 및 제약 조건의 변수는 부울입니다, 즉 0 또는 1이어야 합니다. 의사 부울 최적화는 여러 종류의 최적화 문제를 해결하는데 사용될 수 있습니다. 이 Minisat+ 버전은 제약 계수에 대한 bignum 지원으로 컴파일 되었습니다.
|
|
mona
|
Versions of package mona |
Release | Version | Architectures |
bookworm | 1.4-18-1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
stretch | 1.4-17-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
buster | 1.4-17-1 | amd64,arm64,armhf,i386 |
trixie | 1.4-18-1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
jessie | 1.4-15-1 | amd64,armel,armhf,i386 |
sid | 1.4-18-1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
bullseye | 1.4-17-2 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
Debtags of package mona: |
field | mathematics |
role | program |
scope | utility |
|
License: DFSG free
|
MONA는 논리 WS1S 또는 WS2S 공식을 BDD로 표시되는 유한 상태 오토마타로 변경하는 도구입니다. 공식은 검색 패턴, 반응 시스템의 시간적인 속성, 구문 분석 트리 제약등을 표현할 수 있습니다. 또한 MONA는 컴파일에서 비롯된 자동화를 분석하고, 공식이 유효한지 여부를 판단하며 그렇지 않으면 그 반대 예를 생성합니다.
문서는 MONA 웹사이트에서 구할 수 있습니다.
http://www.brics.dk/mona/.
|
|
picosat
|
Versions of package picosat |
Release | Version | Architectures |
sid | 965-2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
jessie | 960-1 | amd64,armel,armhf,i386 |
stretch | 960-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
buster | 960-1 | amd64,arm64,armhf,i386 |
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,riscv64,s390x |
Debtags of package picosat: |
field | mathematics |
role | program |
|
License: DFSG free
|
부울 공식 (SAT)의 만족도 문제에 대한 NP 완전성에도 불구하고, SAT 솔버는 자주 합리적인 시간 프레임 내에서 이 문제를 결정할 수 있습니다. 다른 모든 NP 전체 문제가 SAT로 축소 될 수 있기 때문에, 솔버는 이 문제 클래스를 위한 범용 도구가 되었습니다.
PicoSAT는 산업용 인스턴스에서 MiniSAT 2.0보다 속도가 더 빠르다고 판명된 SAT 솔버이며, 또한 증명 및 코어를 메모리에 생성할 수 있습니다.
|
|
proofgeneral
generic frontend for proof assistants
|
Versions of package proofgeneral |
Release | Version | Architectures |
stretch | 4.4.1~pre170114-1 | all |
bullseye | 4.4.1~pre170114-1.2 | all |
bookworm | 4.4.1~pre170114-1.2 | all |
trixie | 4.5-3 | all |
sid | 4.5-3 | all |
jessie | 4.3~pre131011-0.2 | all |
Debtags of package proofgeneral: |
field | mathematics |
interface | text-mode, x11 |
role | plugin |
suite | emacs |
use | editing |
|
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.)
|
|
prover9
theorem prover and countermodel generator
|
Versions of package prover9 |
Release | Version | Architectures |
buster | 0.0.200911a-2.1 | amd64,arm64,armhf,i386 |
jessie | 0.0.200911a-2.1 | amd64,armel,armhf,i386 |
stretch | 0.0.200911a-2.1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
|
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
자바에서 SAT 솔버에 대한 효율적인 라이브러리
|
Versions of package sat4j |
Release | Version | Architectures |
stretch | 2.3.5-0.2 | all |
jessie | 2.3.3-1 | all |
buster | 2.3.5-0.3 | all |
sid | 2.3.5-0.3 | all |
trixie | 2.3.5-0.3 | all |
bullseye | 2.3.5-0.3 | all |
bookworm | 2.3.5-0.3 | all |
Debtags of package sat4j: |
field | mathematics |
role | program, shared-lib |
|
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 |
Release | Version | Architectures |
sid | 3.9-1.1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
jessie | 3.7-3 | amd64,armel,armhf,i386 |
trixie | 3.9-1.1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
bullseye | 3.9-1.1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bookworm | 3.9-1.1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
stretch | 3.7-4 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
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,armhf,i386 |
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 |
|
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.
|
|
why3
Software verification platform
|
Versions of package why3 |
Release | Version | Architectures |
buster | 1.2.0-1 | amd64,arm64,armhf,i386 |
trixie | 1.7.2-2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
bookworm | 1.5.1-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 |
sid | 1.7.2-2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
bullseye | 1.3.3-1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
|
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.13.3-1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,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,armhf,i386 |
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.13.3-1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
|
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 |
jessie | 1.7.6+dfsg1-1 | amd64,armel,armhf,i386 |
trixie | 1.8.4+dfsg-2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
sid | 1.8.4+dfsg-2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
buster | 1.8.3-2 | amd64,arm64,armhf,i386 |
bullseye | 1.8.3-3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
stretch | 1.7.6+dfsg1-2 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
bookworm | 1.8.3-3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
|
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.
|
|
|