Debian Science Logic packages

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

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

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

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.

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

En grafisk grænseflade for Coq tilbydes i pakken coqide. Coq kan også bruges med ProofGeneral, som tillader at beviser redigeres med emacs og xemacs. Dette kræver at pakken proofgeneral er installeret.

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

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.

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.

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.

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

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.

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.

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

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.

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

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.

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

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

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.