Dit is de commando-otter die kan worden uitgevoerd in de gratis hostingprovider van OnWorks met behulp van een van onze meerdere gratis online werkstations zoals Ubuntu Online, Fedora Online, Windows online-emulator of MAC OS online-emulator
PROGRAMMA:
NAAM
otter - stellingbewijzer in resolutiestijl
KORTE INHOUD
otter < Invoer bestand > output-bestand
PRODUCTBESCHRIJVING
Deze handleiding documenteert in het kort de: otter opdracht.
otter is een programma voor het bewijzen van stellingen in resolutiestijl voor eerste-orde logica met gelijkheid.
otter omvat de gevolgtrekkingsregels binaire resolutie, hyperresolutie, UR-resolutie en
binaire paramodulatie. Sommige van zijn andere mogelijkheden en functies zijn conversie van eerste-
bestel formules naar clausules, voorwaartse en achterwaartse subsumptie, factoring, weging, antwoord
letterlijke termen, termordening, voorwaartse en achterwaartse demodulatie, evalueerbare functies en
predicaten, Knuth-Bendix-voltooiing en de hints-strategie.
OPTIES
Er worden geen opdrachtregelopties geaccepteerd; alle opties worden gegeven in het invoerbestand.
Gebruik otter online met behulp van onworks.net-services
