Debian Science Project
Summary
Logic
Debian Science - pakker til logik

Denne metapakke er en del af Debian Pure Blend »Debian Science« og den installerer pakker relateret til beregningsmæssig logik. Den indeholder transformationsværktøjer til formler, formelløsere specificeret i diverse logik, interaktive bevissystemer 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
Afhængighedsindtastet funktionelt programmeringssprog
Versions of package agda
ReleaseVersionArchitectures
wheezy2.3.0.1-2all
jessie2.4.0.2-2all
sid2.6.0.1-1all
bullseye2.6.0.1-1all
buster2.5.4.1-3all
stretch2.5.1.1-3all
Debtags of package agda:
rolemetapackage
Popcon: 0 users (0 upd.)*
Versions and Archs
License: DFSG free
Git

Agda er et afhængighedsindtastet funktionelt programmeringssprog: Det har induktive familier, som fungerer som Haskells GADT'er, men de kan indekseres af værdier og ikke kun af typer. Programmet har også parameteropsatte moduler, mixfix-operatører, Unicodetegn og en interaktiv grænseflade for Emacs (indtastningskontrollen kan hjælpe med udvikling af din kode).

Agda er også en bevisassistent: Programmet er et interaktivt system for skrivning og kontrol af beviser. Agda er baseret på intuitionistisk typeteori, et fundamentsystem for konstruktiv matematik udviklet af den svenske logiker Per Martin-Löf. Programmet har mange ligheder med andre bevisassistenter baseret på afhængighedstyper, såsom Coq, Epigram og NuPRL.

Dette er en metapakke, som tilbyder Agdas tilstand for Emacs, kørbar fil, standardbibliotek og programmets dokumentation.

Alt-ergo
Automatisk teorem-bevisfører dedikeret til programverifikation
Versions of package alt-ergo
ReleaseVersionArchitectures
bullseye2.0.0-5amd64,arm64,armel,i386,mips64el,mipsel,ppc64el,s390x
stretch1.30-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
squeeze0.91-2amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy0.94-2amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie0.95.2-3amd64,armel,armhf,i386
sid2.0.0-5amd64,arm64,armel,i386,mips64el,mipsel,ppc64el,s390x
buster2.0.0-3amd64,arm64,armel,i386,mips,mips64el,mipsel,ppc64el,s390x
Debtags of package alt-ergo:
roleprogram
uitoolkitgtk
Popcon: 10 users (17 upd.)*
Versions and Archs
License: DFSG free
Git

Alt-Ergo er en automatisk teorem-bevisfører dedikeret til programverifikation. Alt-Ergo er baseret på CC(X), en kongruent lukkealgoritme som er parameteriseret af en ligningsmæssig teori X. Alt-Ergo har indbyggede bevisførere for sætningslogik, lineær aritmetik, ufortolkede funktionssymboler, associative-kommutative funktionssymboler, polymorfiske arrayer, brugerdefinerede polymorfiske posttyper og polymorfiske nummereringstyper. Programmet har begrænset understøttelse for belysning af arbitrære brugerdefinerede algebraiske typer, første grads kvantorer og ikkelineær aritmetik.

Denne pakke indeholder bevisføreren som en kørbar fil for kommandolinjen samt den grafiske brugerflade.

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

Boolector er en effektiv SMT-løser for den kvantifikatorfrie teori for bit-vektorer i kombination med kvantifikatorfrie ekstensionelle teoriarrayer.

Clasp
Konfliktdrevet nogood-løsningsprogram for svarsæt til indlæring
Versions of package clasp
ReleaseVersionArchitectures
jessie3.1.0-1amd64,armel,armhf,i386
wheezy2.0.6-2amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
sid3.3.4-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bullseye3.3.4-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
buster3.3.4-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch3.2.1-3amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
upstream3.3.5
Debtags of package clasp:
roleprogram
Popcon: 66 users (45 upd.)*
Newer upstream!
License: DFSG free
Git

Clasp er et løsningsprogram for svarsæt (udvidet) til normale logiske programmer. Det kombinerer modelleringsfunktionerne, på højt niveau, for svarsætprogrammering (ASP) med moderne teknikker fra området med boolesk begrænsningsløsning. Den primære clasp-algoritme beror på konfliktdreven nogood-indlæring, en teknik, der viste sig at have høj succes for opfyldelighedskontrol (SAT). I modsætning til andre løsningsprogrammer for indlærings-ASP, så stoler clasp ikke på forældede programmer, såsom et SAT-løsningsprogram eller ethvert andet eksisterende ASP-løsningsprogram. Snarere har clasp været udviklet til svarsæt-løsning baseret på konfliktdrevet nogood-indlæring. Clasp kan anvendes som et ASP-løsningsprogram (på LPARSE-uddataformat), som et SAT-løsningsprogrammet (på forenklet DIMACS/CNF-format) eller som et PB-løsningsprogram (på OPB-format).

Coala
Oversætter action-sprog til programmer med svarsæt
Versions of package coala
ReleaseVersionArchitectures
jessie1.0.1-5amd64,armel,armhf,i386
wheezy1.0.1-5amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
Debtags of package coala:
roleprogram
Popcon: 0 users (0 upd.)*
Versions and Archs
License: DFSG free
Git

Værktøjet coala oversætter et action-sprog til et logisk program, under semantikken for svarsæt. Efter at være grundet af lparse eller gringo, kan logikprogrammet løses med en løsningsfunktion for svarsæt såsom clasp. I øjeblikket kan coala oversætte action-sprogene AL, B, C, et delsæt af C+ og action-sproget CTAID. Typen af inddatasprog kan angives med et tilvalg i kommandolinjen.

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

Cbc (Coin-or branch and cut) er en blandet heltals programmeringsløser udviklet i åben kildekode og skrevet i C++. Den kan bruges som et bibliotek, der kan kaldes eller som en uafhængig kørbar fil.

Denne pakke indeholder kørbare filer for cbc.

Coinor-symphony
COIN-OR-løser for blandede-heltals lineære programmer
Versions of package coinor-symphony
ReleaseVersionArchitectures
buster5.6.16+repack1-1.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie5.6.1-1amd64,armel,armhf,i386
stretch5.6.1-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye5.6.16+repack1-1.1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
sid5.6.16+repack1-1.1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
upstream5.6.17
Popcon: 18 users (4 upd.)*
Newer upstream!
License: DFSG free
Git

SYMPHONY er en generisk blandet-heltals lineær programløser (MILP). Udviklet i åben kildekode som et kaldbart bibliotek og med en udvidelig ramme for implementering af tilpassede løsere. SYMPHONY har et antal avancerede funktioner, inklusiv evnen til at løse fler-objektive MILP'er, evnen til at forvarme sine løsningsprocedure og evnen til at udføre grundlæggende følsomhedsanalyser.

SYMPHONY er en del af det større COIN-OR-initiativ (Computational Infrastructure for Operations Research).

Denne pakke indeholder symphony's kørbare fil.

Coq
Bevisassistent for højere ordens logik - topniveau og kompiler
Versions of package coq
ReleaseVersionArchitectures
sid8.9.1-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bullseye8.9.1-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
squeeze8.2.pl2+dfsg-1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy8.3.pl4+dfsg-2amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie8.4pl4dfsg-1amd64,armel,armhf,i386
buster8.9.0-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch8.6-4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
upstream8.10.2
Debtags of package coq:
develcompiler
fieldmathematics
interfacecommandline, text-mode
roleprogram
scopeutility
uitoolkitncurses
Popcon: 48 users (53 upd.)*
Newer upstream!
License: DFSG free
Git

Coq er en bevisassistent for højere ordens logik, som tillader udviklingen af computerprogrammer som overholder deres formelle specifikationer. Det udvikles med brug af Objective Caml og Camlp5.

Denne pakke tilbyder coqtop, en kommandolinjegrænseflade til Coq.

Pakken proofgeneral gør at beviser kan redigeres via Emacs og XEmacs.

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

CVC3 er en automatisk læresætningbeviser for Satisfiability Modulo Theories-problemer (SMT). Den kan bruges til at bevise validiteten (eller, samtidig, opfyldelighed) for 1. orden formler i et stort antal af indbyggede logiske teorier og deres kombinationer.

CVC3 er det sidste skud på stammen i en serie af populære SMT-bevisere, som udsprang fra Stanford University med SVC-systemet. Det bygger specifikt på kodebasen for CVC Lite, dets seneste forgænger. Dets design på højt niveau følger Sammy-beviseren.

CVC3 fungerer med en version af 1. orden logik med polymorfiske typer og har en bred række af funktioner inklusive:

  • flere indbyggede basisteorier: rationel og heltals lineær aritmetik, arrayer, tupler, poster, induktive datatyper, bit- vektorer og lighed over ufortolkede funktionssymboler
  • understøttelse for kvantorer
  • en interaktiv tekstbaseret grænseflade
  • rig C, C++ og Java API'er for indlejring i andre systemer
  • evner indenfor bevis- og modeloprettelse
  • prædikat undertypebestemmelse
  • grundlæggende ingen begrænsning på dens brug for forskning eller kommercielle formål (se licensbeskrivelsen)

Denne pakke indeholder CVC3-kommandolinjeprogrammet.

The package is enhanced by the following packages: cvc3-el
Cvc4
Automatiseret læresætningsbeviser for SMT-problemer
Versions of package cvc4
ReleaseVersionArchitectures
buster1.6-2amd64,i386,mips,mips64el,mipsel
bullseye1.6-2amd64,i386,mips64el,mipsel
sid1.6-2amd64,i386,mips64el,mipsel
Popcon: 8 users (5 upd.)*
Versions and Archs
License: DFSG free
Git

CVC4 er en effektiv automatisk læresætningsbeviser for satisfiability modulo theories-problemer (SMT). Den kan bruges til at bevise validiteten (eller, samtidig, opfyldelsen) af første orden formler i et stort antal indbyggede logiske teorier og deres kombination.

CVC4 er lavet som en åben SMT-motor, der kan udvides. Den kan bruges som et uafhængigt værktøj eller som et bibliotek. Det er den fjerde i Cooperating Validity Checker-familien indenfor værktøjer (også inkluderende CVC, CVC Lite og CVC3). CVC4 er blevet designet til at øge ydelsen og reducere hukommelsesforbruget i forhold til tidligere versioner.

Denne pakke indeholder binære filer krævet til at bruge CVC4 som et uafhængigt værktøj.

Depqbf
Beviser for kvantificerede booleske formler
Versions of package depqbf
ReleaseVersionArchitectures
buster5.01-3amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye5.01-3amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
sid5.01-3amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
jessie3.04-1amd64,armel,armhf,i386
wheezy0.1-1amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
stretch5.01-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
upstream6.03
Popcon: 6 users (2 upd.)*
Newer upstream!
License: DFSG free
Git

DepQBF er en søgningsbaseret beviser for kvantificerede booleske formler (QBF) i prenex konjunktiv normalform. Den er baseret på DPLL-algoritmen til QBF, kaldet QDPLL, med konflikt-drevne klausul og løsningsdrevet terninglæring. Ved at analysere den syntaktiske struktur af en formel, forsøger DepQBF at identificere uafhængige variabler. I almindelighed kan information på uafhængige variable være repræsenteret i de formelle rammer for afhængighedsordninger. DepQBF beregner den såkaldte »standardafhængighedsordning« hos en given formel. Udover andre fordele øger information på uafhængige variabler ofte friheden til beslutningstagning og klausul læring.

Gringo
Grundlæggende værktøjer for (disjunktive) logikprogrammer
Versions of package gringo
ReleaseVersionArchitectures
wheezy3.0.4-3amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie4.4.0-1amd64,armel,armhf,i386
stretch5.1.0-4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster5.3.0-10amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye5.3.0-10amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
sid5.3.0-10amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
upstream5.4.0
Debtags of package gringo:
roleprogram
Popcon: 75 users (43 upd.)*
Newer upstream!
License: DFSG free
Git

På nuværende tidspunkt fungerer løsningsfunktioner for svarsæt på programmer uden variabler. Derfor er der brug for en grundlægger (»grounder«) der, givet et input-program med førsteordens variabler, beregner et ækvivalent (variabelfrit) grundprogram.

Denne pakke indeholder følgende værktøjer:

  • gringo: en grunder som via et inddataprogram med første-orden variabler, beregner et tilsvarende grundprogram (variabel-fri) i aspif-format. Dets uddata kan behandles yderligere med svarsæt solver-clasp. Startende med gringos serie 5, er dets uddata ikke længere direkte kompatible med løsere såsom smodels eller cmodels der læser smodels-format. Brug lpconvert til at oversætte aspif- formatet til smodels-formatet.
  • clingo: kombinerer både gringo og clasp til et monolitisk system. På den måde tilbyder programmer mere kontrol over grunding og løsning af proces end gringo og clasp kan tilbyde individuelt: multi-shot løsning.
  • lpconvert: konverterer mellem gringos aspif- og smodels-format.
  • reify: lille redskab som abstraherer et logisk program, givet i apif- format. Det fremstiller et sæt af fakta, som kan viderebehandles med 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 - læresætningsbevis
Versions of package hol-light
ReleaseVersionArchitectures
sid20190729-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
wheezy20120602-1amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie20131026-1amd64,armel,armhf,i386
stretch20170109-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Popcon: 2 users (0 upd.)*
Versions and Archs
License: DFSG free
Git

HOL Light en interaktivt læresætningsbeviser for Higer-Order Logic med en meget simpel logisk kerne kørende i et OCaml-topniveau. HOL Light er kendt for verifikation af kommatalsaritmetik samt for projektet Flyspeck, der forsøger at formalisere Tom Hales' bevis for Keplerformodningen.

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

HOL-systemet er et miljø for interaktive beviser for læresætninger i en højere logik. Dens mest imponerende funktion er dens høje grad af programmerbarhed via metasproget ML. Systemet har en bred vifte af brug fra formalisering af ren matematik til verificering af industriel programmel. Akademiske og industrielle sider over hele verden bruger HOL.

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

Dette program konverterer en lineær temporal logik-formel (ltl) til en generaliseret Büchi-automat. Den resulterende automat kan bruges, for eksempel, i modelkontrol, hvor den repræsenterer en egenskab, som skal verificeres fra en model (f.eks. et Petri-net).

Mace2
program som søger efter finitte modeller for førstegradsudtryk
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 er et program som søger i finitte modeller for førstegradsudtryk og ligningsmæssige udtryk. Det udvikles af Argonne National Laboratory.

Denne pakke inkluderer ANLDP, som kalder den udsagnsmæssige beslutningsprocedure direkte i kernen af MACE.

MACE fungerer som komplementær følgesvend til OTTER, som søger efter gendrivelser af den samme klasse af udtryk. Specielt hvis du har en førstegradsformodning vil OTTER søge efter et bevis, og MACE vil søge for et modeksempel fra den samme inddatafil.

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

Maria er et funktionsrigt værktøj designet til at hjælpe ingeniører med at modellere og løse relaterede problemer vedrørende samtidighed i parallelle og distribuerede computersystemer.

Maria finder døde ender og overtrædelser mod sikkerhed eller oppetidskrav ved at undersøge alle tilstande som kan nås fra den oprindelige tilstand for et system. Værktøjet håndterer ti eller hundredvis af millioner af tilgængelige tilstande og aktiverede handlinger.

Den imponerende kraft i Marias formalisme er tæt på programmeringssprog på højt niveau, takket være sit rige datatypesystem og funktionsrige algebraiske udregninger.

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

Matita er en grafisk interaktiv læresætningsbeviser baseret på Calculus of (Co)Inductive Constructions.

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

Maude er et højtydende reflekterende sprog og system, der understøtter både equational og omskrivning af logisk specifikation og programmering for en bred vifte af programmer. Maude er blevet påvirket i væsentlig grad af OBJ3-sproget, hvilket kan betragtes som et equational logik-undersprog. Ud over at støtte equational specifikation og programmering understøtter Maude også omskrivning af logikberegning.

Omskrivning af logik er en logik af samtidige ændringer, som naturligt kan håndtere sig med tilstanden og de samtidige beregninger. Programmet har gode egenskaber som en generel semantisk ramme til at give eksekverbar semantik til en lang række sprog og modeller af samtidighed. Specielt understøttes samtidig objektorienteret beregning rigtig godt. De samme grunde som gør omskrivning af logik til en god semantisk ramme gør det også til en god logisk ramme, d.v.s. en metalogik hvor mange andre logikker kan repræsenteres naturligt og køres.

Maude understøtter på en systematisk og effektiv måde logisk refleksion. Dette gør Maude bemærkelsesværdig udvidelig og funktionsrig, understøtter en udvidelig algebra af modulsammensætningsoperationer og giver mange avancerede metaprogrammerings- og metasprog-anvendelser. Faktisk er nogle af de mest interessante anvendelser af Maude metasprog-programmer, hvor Maude bruges til at oprette eksekverbare miljøer for forskellige logikker, læresætningsbeviser, sprog og beregningsmodeller.

Maude er af interesse for det biomedicinske samfund til modellering og analyse af biologiske systemer.

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

MinSat+ er en løser for pseudo-boolesk optimering (AKA 0-1- heltalsprogrammering), som er baseret på MiniSAT SAT-solver. Programmer understøtter optimering af lineær objektiv funktion, emne til et sæt af lineære begrænsninger. Variablerne for objektivfunktionen og begrænsningerne er booleske, dvs. krævet at være 0 eller 1. Pseudo- boolesk optimering kan bruges til at løse mange slags kombinatoriske optimeringsproblemer. Denne version af Minisat+ er kompileret med understøttelse af Bignum for begrænsningskoefficienter.

Mona
teorem-bevisførelse baseret på automat
Versions of package mona
ReleaseVersionArchitectures
squeeze1.4-13-1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
buster1.4-17-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch1.4-17-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie1.4-15-1amd64,armel,armhf,i386
wheezy1.4-13-3amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
sid1.4-17-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bullseye1.4-17-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
Debtags of package mona:
fieldmathematics
roleprogram
scopeutility
Popcon: 8 users (2 upd.)*
Versions and Archs
License: DFSG free
Git

MONA er et værktøj som oversætter formler i logikken fra WS1S eller WS2S til automater med finitte tilstande repræsenteret af BDD'er. Formlerne kan udtrykke søgemønstre, temporale egenskaber fra reaktive systemer, begrænsninger i fortolkningstræer, osv. MONA analyserer også den automat, der resulterer fra kompileringen, afgør om formlen er gyldig og genererer, forudsat at formlen er gyldig, et modeksempel.

Dokumentationen er tilgængelig fra MONAs hjemmeside, http://www.brics.dk/mona/.

Picosat
SAT-løser med proof- og core-understøttelse
Versions of package picosat
ReleaseVersionArchitectures
stretch960-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie960-1amd64,armel,armhf,i386
wheezy936-4amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
squeeze913-4amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
sid965-1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bullseye965-1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
buster960-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Debtags of package picosat:
fieldmathematics
roleprogram
Popcon: 11 users (0 upd.)*
Versions and Archs
License: DFSG free
Git

På trods af NP-fuldstændigheden i opfyldelighedsproblemet for booleske formler (SAT) er SAT-løsere ofte bedre i stand til at bestemme dette problem på en fornuftig tid. Da alle andre NP-fuldstændige problemer kan reduceres til SAT, er løserne blevet et alment værktøj for denne problemklasse.

PicoSAT er en SAT-løser, som viste sig at være hurtigere på industrielle instanser end MiniSAT 2.0 og kan også oprette proof'er og core'r i hukommelsen.

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

Proof General er en major-tilstand til at omdanne Emacs til en interaktiv bevisassistent for skrivning af matematiske beviser med brug af en række læresætningsbevisere.

Denne pakke tilbyder Proof General-understøttelse for Coq. (Der er ingen andre bevisassistenter som man med fornuft kan understøtte).

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
bevisudførelse for teoremer og oprettelsesmodel for modmodel
Versions of package prover9
ReleaseVersionArchitectures
squeeze0.0.200902a-2amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
jessie0.0.200911a-2.1amd64,armel,armhf,i386
stretch0.0.200911a-2.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster0.0.200911a-2.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
wheezy0.0.200902a-2.1amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
Popcon: 36 users (10 upd.)*
Versions and Archs
License: DFSG free
Bzr

Denne pakke tilbyder Prover9's bevissystem for resolutioner/paramodulation og Mace4's opretter af modbeviser.

Prover9 foretager automatiserede bevisudførelser for teoremer i prædikatlogik og ligningslogik. Det er efterfølgeren for Otter- bevissystemet for teoremer. Prover9 bruger de samme slutningsteknikker for ordnede resolutioner og paramodulering med udvælgelse af literaler.

Programmet Mace4 søger efter finitte strukturer, der tilfredsstiller prædikatlogik og ligningslogik, den samme slags udtryk som Prover9 accepterer. Hvis påstanden en afvisning af en antagelse, så vil alle strukturer som Mace4 finder, være modeksempler på antagelsen.

Mace4 kan være et værdifuldt tillæg til Prover9, der kigger efter modeksempler før (eller på samme tid som) brug af Prover9 til at søge efter et bevis. Programmet kan også bruges til at hjælpe med at fejlsøge inddata-klausuler og formler for Prover9.

Sat4j
Effektivt bibliotek af SAT-løsere i Java
Versions of package sat4j
ReleaseVersionArchitectures
bullseye2.3.5-0.3all
stretch2.3.5-0.2all
jessie2.3.3-1all
squeeze2.2.0-3all
wheezy2.3.1-1all
sid2.3.5-0.3all
buster2.3.5-0.3all
Debtags of package sat4j:
fieldmathematics
roleprogram, shared-lib
Popcon: 209 users (47 upd.)*
Versions and Archs
License: DFSG free

Formålet med SAT4J-biblioteket er at tilbyde et effektivt bibliotek af SAT-løsere i Java. Sammenlignet med OpenSAT-projektet, har SAT4J-biblioteket som målgruppe førstegangsbrugere af SAT »sorte bokse«, som vil indlejre SAT-teknologier i deres program uden at bekymre sig om detaljerne. SAT4J-projektet forsøger også at tilbyde et grundlæggende arbejde for SAT-forskere.

Spass
Automatiseret læresætningsbeviser for første orden logik med ligestilling
Versions of package spass
ReleaseVersionArchitectures
squeeze3.7-2amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
stretch3.7-4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
sid3.7-4amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
wheezy3.7-3amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie3.7-3amd64,armel,armhf,i386
Debtags of package spass:
fieldmathematics
Popcon: 5 users (0 upd.)*
Versions and Archs
License: DFSG free
Git

SPASS er en mætningsbaseret automatiseret læresætningsbeviser for første ordens logik med ligestilling. Det er unikt på grund af kombinationen af superposition calculus med særlige regler følgeslutning/reduktion for sortering (typer) og en opsplitningsregel for tilfældeanalyse motiveret af beta-reglen om analytiske tableauer og sagsanalyse anvendt i Davis-Putnam-proceduren. Endvidere tilbyder SPASS en sofistikeret klausulnormalformsoversættelse.

Denne pakke består af den SPASS/FLOTTER-binære fil, dokumentation og en lille eksempelsamling. Værktøjssamlingerne indeholder beviskontrol-pcs, syntaksoversætterne dfg2otter og dfg2tptp og ASCII pretty-printeren dfg2ascii.

Toulbar2
Præcis kombinatorisk optimering for grafiske modeller
Versions of package toulbar2
ReleaseVersionArchitectures
buster1.0.0+dfsg3-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye1.0.0+dfsg3-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
sid1.0.0+dfsg3-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
Popcon: 7 users (4 upd.)*
Versions and Archs
License: DFSG free
Git

Toulbar2 er et præcist diskret optimeringsværktøj for grafiske modeller såsom Cost Function Networks, Markov Random Fields, Weighted Constraint Satisfaction Problems og Bayesian Nets.

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

Why forsøger at være en »verification conditions generator«-motor (VCG) for andre verificeringsværktøjer. Programmet tilbyder et funktionsrigt inddatasprog inklusive højere funktioner, polymorfisme, referencer, array'er og undtagelser. Programmet oprette bevisobligationer for mange systemer: Bevisassistenterne Coq, PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar og beslutningsprocedurerne Simplify, Alt-Ergo, Yices, CVC Lite og haRVey.

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

Why3 er en platform for deduktiv programverifikation. Den tilbyder et rigt sprog for specifikation og programmering, kaldt WhyML, og afhænger af eksterne læresætningsbevisere, både automatiserede og interaktive, til at fjerne verifikationsbetingelser. Why3 har et standardbibliotek med logiske teorier (heltal og reel aritmetik, booleske operationer (tabeller, køer, hashtabeller etc.). En bruger kan skrive WhyML-programmer direkte og hente korrekt-efter-konstruktion OCaml-programmer via en automatiseret udtrækningsmekanisme. WhyML bruges også som et mellemliggende sprog for verifikation af C-, Java-, eller Ada-programmer.

Why3 er en fuldstændig ny implementering af den tidligere Why-platform. Blandt de nye funktioner er: utallige udvidelser for inddatasproget, en ny arkitektur for kald af eksterne bevisere, og en veldesignet API, der giver mulighed for at bruge Why3 som et programbibliotek. En vigtig del er lagt på modulopbygning og typeparametrisering, hvilket giver slutbrugeren en mulighed for nemt at genbruge Why3-formaliseringer eller tilføje understøttelse for en ny ekstern beviser hvis ønsket.

Z3
Læresætningsbeviser fra Microsoft Research
Versions of package z3
ReleaseVersionArchitectures
stretch4.4.1-1~deb9u1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
sid4.8.7-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bullseye4.8.6-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
buster4.4.1-1~deb10u1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Popcon: 21 users (38 upd.)*
Versions and Archs
License: DFSG free
Git

Z3 er en moderne læresætningsbeviser fra Microsoft Research. Den kan bruges til at kontrollere opfyldelsen for logiske formler over en eller flere teorier. Z3 tilbyder et overbevisende match for programanalyse og verifikationsværktøjer da flere gængse programkonstruktioner oversættes direkte til understøttede teorier.

Z3-inddataformatet er en udvidelse af det defineret af SMT-LIB 2.0-standarden.

Official Debian packages with lower relevance

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

Coin-MP-optimeringsprogrammet er en løser, udviklet i åben kildekode, som er en del af COIN-OR-projektet, som er et initiativ der skal øge udvikling af programmer udviklet i åben kildekode for forskningsfællesskabet indenfor operation.

CoinMP er et C-API-bibliotek, som understøtter det meste af funktionalitetet i CLP (Coin LP)-, CBC (Coin Branch-and-Cut)- og CGL (Cut Generation Library)-projekter.

Denne pakke indeholder filerne krævet for at bygge programmer, der bruger libCoinMP.

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