Otter (satsbevisare)
| Originalförfattare | William McCune |
|---|---|
| Skrivet i | C |
| Typ | Automatiserad teorembevisande |
| Hemsida |
|
Otter är en automatiserad teoremprover utvecklad av William McCune vid Argonne National Laboratory i Illinois. Otter var den första allmänt spridda, högpresterande teorembevisaren för första ordningens logik , och den banade väg för ett antal viktiga implementeringstekniker. Otter är en akronym för Organized Techniques for Theorem-proving and Effective Research .
Beskrivning
Otter är baserad på upplösning och paramodulering, begränsad av termordningar liknande de i superpositionskalkylen . Beviset stöder också positiv och negativ hyperupplösning och en uppsättning stödstrategi. Bevissökning baseras på mättnad med en version av algoritmen för given sats och styrs av flera heuristiker. Det finns också metaheuristik som bestämmer sökparametrar automatiskt. Otter var också banbrytande för användningen av effektiva termindexeringstekniker för att påskynda sökandet efter slutledningspartners i stora klausuluppsättningar.
Uttern har varit mycket stabil under ett antal år men utvecklas inte längre aktivt. Från och med november 2008 var den sista ändringsloggen den 14 september 2004. En efterträdare till Otter är Prover9 .
Programvaran är allmän egendom . University of Chicago har avböjt att hävda sina upphovsrätter till denna programvara, och den kan användas, modifieras och omdistribueras (med eller utan ändringar) av allmänheten. "VARKEN USA:S REGERING ELLER NÅGON MYNDIGHET AV DESSA [...] REPRENTERAR ATT DESS ANVÄNDNING INTE SKULLE KRÄNKA PRIVAT ÄGDA RÄTTIGHETER."
Enligt Wos och Pieper är OTTER skriven i cirka 28 000 rader C-programmeringsspråk.
Se även
Anteckningar
- Kalman, John Arnold (februari 2001). Automatiserat resonemang med OTTER . Rinton Press. ISBN 978-1589490048 .
externa länkar
- Otters hemsida
-
"OTTER 3.3 Referensmanual" (PDF) . Arkiverad från originalet 2018-11-13 . Hämtad 2018-11-13 .
{{ citera webben }}: CS1 underhåll: bot: ursprunglig URL-status okänd ( länk )