FLOTTER – Online in der Cloud

PROGRAMM:

NAME/FUNKTION

SPASS – automatisierter Theorembeweiser für vollständige Logik erster Ordnung mit Gleichheit

ZUSAMMENFASSUNG

SPASS [Optionen] [Eingabedatei]

BESCHREIBUNG

SPASS ist ein automatisierter Theorembeweiser für vollständig sortierte Logik erster Ordnung mit Gleichheit
erweitert die Überlagerung um Sortierungen und eine Aufteilungsregel für die Fallanalyse. SPASS kann auch sein
Wird als Modallogik- und Beschreibungslogik-Theorembeweiser verwendet.

OPTIONAL

Befehlszeilenoptionen in SPASS werden durch Änderungen an der GNU-Befehlszeile implementiert
Optionspaket für C. Allein die Angabe der Option setzt ihren Wert auf 1 und bedeutet, dass die Option aktiviert wird
Möglichkeit. Um eine Option zu deaktivieren, muss der Wert durch Deklaration auf 0 gesetzt werden -Option= 0.
Die folgenden Optionen werden derzeit von SPASS unterstützt:

-Auto
Aktiviert/deaktiviert den automatischen Modus, in dem sich SPASS automatisch konfiguriert. Der
Inferenz-/Reduktionsregeln, die Sortiertechnik, die Reihenfolge und Priorität sowie
die Aufteilungs- und Selektionsstrategie sind festgelegt. Im Automatikmodus ist SPASS abgeschlossen. Mischen
Der Auto-Modus mit benutzerdefinierten Optionen kann die Vollständigkeit zerstören. Der Standardwert ist 1.

-Stdin
Aktiviert/deaktiviert die Eingabe in SPASS über stdin. Das Dateiargument wird ignoriert. Der Standardwert ist 0.

-Interaktiv
Aktiviert/deaktiviert den interaktiven Modus. Zuerst erhält SPASS eine Reihe von Axiomen und dann
Der Prüfer übernimmt nachfolgende Beweisaufgaben. Der Standardwert ist 0.

-Flotter
Aktiviert/deaktiviert den CNF-Übersetzungsmodus von SPASS. Wenn die Option gesetzt ist, nur SPASS
Führt eine Klausel-Normalformübersetzung durch. Wenn kein Ausgabedateiargument angegeben wird, wird SPASS angegeben
druckt den CNF auf stdout. Der Standardwert ist 0.

-SOS
Aktiviert/deaktiviert den Satz der Supportstrategie. Der Standardwert ist 0.

-Splits=n
Legt die Anzahl der möglichen Splitting-Anwendungen fest n. Wenn n=-1 dann die Anzahl von
Aufteilungen sind nicht begrenzt. Der Standardwert ist 0.

-Speicher=n
Legt fest, wie viel Speicher SPASS für die Beweissuche zur Verfügung steht n Bytes. Die
Der zum Starten von SPASS benötigte Speicher kann nicht eingeschränkt werden. Der Standardwert ist -1, was bedeutet, dass
Die Speicherzuteilung wird nur durch den verfügbaren Speicher eingeschränkt.

-TimeLimit=n
Legt ein Zeitlimit für die Beweissuche fest n Sekunden. Der Standardwert ist -1, was bedeutet, dass SPASS
kann ewig laufen. Das Zeitlimit wird abgefragt, wenn SPASS eine neue Klausel für auswählt
Schlussfolgerungen. Wenn ein einzelner Inferenzschritt zu einer Explosion der generierten Anzahl führt
Bei Klauseln kann es daher vorkommen, dass eine bestimmte Frist erheblich überschritten wird.

-DocSST
Aktiviert/deaktiviert die Dokumentationsausgabe für statisches Soft Typing. Die verwendete Sortiertheorie als
sowie der (fehlgeschlagene) Beweisversuch für die Sortierbeschränkung wird gedruckt. Der Standardwert ist 0.

-DocProof
Aktiviert/deaktiviert die Beweisdokumentation. Wenn SPASS einen Proof findet, wird dieser schließlich gedruckt.
Wenn SPASS eine Sättigung findet, wird schließlich der gesättigte Satz von Klauseln gedruckt.
Die Aktivierung der Nachweisdokumentation kann die Leistung von SPASS erheblich beeinträchtigen, weil
Der Prüfer muss Klauseln speichern, die andernfalls weggeworfen werden könnten. Der Standardwert ist 0.

-DocSplit
Legt die Dokumentation geteilter Backtracking-Schritte fest. Wenn auf 1 gesetzt, der Strom
Der Backtracking-Level wird gedruckt. Bei der Einstellung 2 wird auch im Falle einer Teilung gedruckt
die zurückverfolgte Klausel zurückverfolgen. Der Standardwert ist 0.

-Schleifen
Legt die maximale Anzahl von Mainloop-Iterationen für SPASS fest. Der Standardwert ist -1.

-PSub
Aktiviert/deaktiviert das Drucken subsumierter Klauseln. Der Standardwert ist 0.

-PRew
Aktiviert/deaktiviert das Drucken einfacher Rewrite-Anwendungen. Der Standardwert ist 0.

-PCon
Aktiviert/deaktiviert das Drucken von Kondensationsanwendungen. Der Standardwert ist 0.

-PTaut
Aktiviert/deaktiviert das Drucken von Tautologie-Löschanwendungen. Der Standardwert ist 0.

-PObv
Aktiviert/deaktiviert das Drucken offensichtlicher Reduktionsanwendungen. Der Standardwert ist 0.

-PSSi
Aktiviert/deaktiviert das Drucken von Sortiervereinfachungsanwendungen. Der Standardwert ist 0.

-PSST
Aktiviert/deaktiviert das Drucken statischer Soft-Typing-Anwendungen. Alle gelöschten Klauseln sind
gedruckt. Der Standardwert ist 0.

-PMRR
Aktiviert/deaktiviert das Drucken von Anwendungen mit passender Ersatzauflösung. Standard ist
0.

-PUnC
Aktiviert/deaktiviert das Drucken von Einheitenkonfliktanwendungen. Der Standardwert ist 0.

-PAED
Aktiviert/deaktiviert das Drucken von Klauseln, in denen redundante Gleichungen entfernt wurden
(Löschung der Zuordnungsgleichung).

-PDer
Aktiviert/deaktiviert das Drucken von durch Rückschlüsse abgeleiteten Klauseln. Der Standardwert ist 0.

-Pgegeben
Aktiviert/deaktiviert das Drucken der angegebenen Klausel, die zum Durchführen von Rückschlüssen ausgewählt wurde.
Standard ist 0.

-PLabels
Aktiviert/deaktiviert das Drucken von Etiketten. Wenn -DocProof gesetzt ist und keine Etiketten für
Formeln werden durch die Eingabe bereitgestellt, SPASS generiert generische Beschriftungen, die dann vorliegen
gedruckt werden, indem Sie diese Option aktivieren. Der Standardwert ist 0.

-PGehalten
Aktiviert/deaktiviert das Drucken beibehaltener Klauseln. Dies sind Klauseln, die durch Schlussfolgerungen generiert werden
(Backtracking), die nicht redundant sind. Bei der Eingabe abgeleitete Klauseln
Reduzierung/Sättigung werden nicht gedruckt. Der Standardwert ist 0.

-PProblem
Aktiviert/deaktiviert das Drucken des Eingabeklauselsatzes. Der Standardwert ist 1.

-PEmptyClause
Aktiviert/deaktiviert das Drucken abgeleiteter leerer Klauseln. Der Standardwert ist 0.

-PStatistic
Aktiviert/deaktiviert das Drucken einer endgültigen Statistik zu abgeleiteten/zurückverfolgten/behaltenen Klauseln.
durchgeführte Teilungen, genutzte Zeit und genutzter Platz. Der Standardwert ist 1.

-FPModel
Aktiviert/deaktiviert die Ausgabe eines eventuell gefundenen Modells in eine Datei. Wenn auf 1 gesetzt, alle
Klauseln im endgültigen Satz werden gedruckt. Wenn auf 2 gesetzt, nur potenziell produktive Klauseln
gedruckt werden, das sind Klauseln ohne ausgewähltes negatives Literal und ein maximales positives
eins. Wenn ist der Name des Eingabeproblems und des letztendlich generierten Problems
Wenn der Satz gesättigt ist, wird die Sättigung in die Datei gedruckt .Modell, für
sonst zu .Klauseln. Letzterer Fall kann z. B. durch eine Zeit verursacht werden
Grenze. Der Standardwert ist 0.

-FPDFGProof
Aktiviert/deaktiviert die Ausgabe eines eventuell gefundenen Beweises in eine Datei. Verwenden dieser Option
erfordert die Einstellung der Option -DocProof. Wenn ist der Name der Eingabe
Problem, auf das der Proof gedruckt wird .prf. Der Standardwert ist 0.

-PFlags
Aktiviert/deaktiviert die Ausgabe aller Flagwerte. Die Flaggeneinstellungen werden am ausgedruckt
Ende eines SPASS-Laufs in Form eines DFG-Syntax-Eingabeabschnitts. Der Standardwert ist 0.

-POptSkolem
Aktiviert/deaktiviert die Ausgabe optimierter Skolemisierungsanwendungen. Der Standardwert ist 0.

-PStrSkolem
Aktiviert/deaktiviert die Ausgabe starker Skolemisierungsanwendungen. Der Standardwert ist 0.

-PBDC
Aktiviert/deaktiviert die Ausgabe von Klauseln, die aufgrund gebundener Einschränkungen gelöscht wurden. Standard
ist 0.

-PBInc
Aktiviert/deaktiviert die Ausgabe gebundener Einschränkungsänderungen. Der Standardwert ist 0.

-PApplyDefs
Aktiviert/deaktiviert das Drucken von Erweiterungen von Atomdefinitionen. Der Standardwert ist 0.

-Wählen
Legt die Auswahlstrategie für SPASS fest. Wenn auf 0 gesetzt, erfolgt keine Auswahl negativer Literale
erledigt. Wenn auf einen anderen Wert festgelegt, ist höchstens ein negatives Literal in einer Klausel vorhanden
ausgewählt. Wenn auf 1 gesetzt, negative Literale in Klauseln mit mehr als einem maximalen Literal
ausgewählt sind. Entweder ein negatives Literal mit einem Prädikat aus der Auswahlliste (siehe
unten) wird ausgewählt oder, wenn kein solches negatives Literal verfügbar ist, ein negatives Literal mit
maximales Gewicht gewählt wird. Bei Einstellung auf 2 werden immer negative Literale ausgewählt. Wieder,
entweder ein negatives Literal mit einem Prädikat aus der Auswahlliste (siehe unten).
gewählt oder wenn kein solches negatives Literal verfügbar ist, ein negatives Literal mit Maximum
Gewicht gewählt wird. Im letzteren Fall kommt es zu einem geordneten hyperauflösungsähnlichen Verhalten
der angeordneten Auflösung. Wenn auf 3 gesetzt, jedes negative Literal mit einem Prädikat, das durch angegeben wird
die Auswahlliste (siehe unten) ist ausgewählt. Der Standardwert ist 1.

-RInput
Aktiviert/deaktiviert die Reduzierung des anfänglichen Klauselsatzes. Der Standardwert ist 1.

-Sorten
Bestimmt die monadischen Literale, die die Sortierbeschränkung für die Anfangsklausel erstellt haben
Satz. Wenn der Wert auf 0 gesetzt ist, wird keine Sortierbeschränkung erstellt. Wenn auf 1 gesetzt, sind alle negativen Monaden
Literale mit einer Variablen als Argument bilden die Sortierbeschränkung. Wenn auf 2 gesetzt, alle
Negative monadische Literale bilden die Sortierbeschränkung. Die Einstellung von -Sorts auf 2 kann schädlich sein
Der Vollständigkeit halber, da Sortierbeschränkungen der Grundstrategie und der Statik unterliegen
sanftes Tippen. Der Standardwert ist 1.

-SatInput
Aktiviert/deaktiviert die Eingangssättigung. Die Sättigung ist unvollständig, wird aber garantiert
beenden. Der Standardwert ist 0.

-WDRatio
Legt das Verhältnis zwischen bestimmten Klauseln fest, die nach Gewicht oder Tiefe in der Suche ausgewählt werden
Raum. Das Gewicht ist die Summe aller Symbolgewichte, die durch -FuncWeight und bestimmt werden
-VarWeight-Optionen. Die Tiefe aller anfänglichen Klauseln beträgt 0 und der von erzeugten Klauseln
Rückschlüsse erhalten die maximale Tiefe einer übergeordneten Klausel plus 1. Der Standardwert ist 5, d. h
dass 4 Klauseln nach Gewicht und die fünfte Klausel nach Tiefe ausgewählt werden.

-PrefCon
Legt das Verhältnis zur Berechnung der Gewichtung für Vermutungsklauseln fest und ermöglicht dies
bevorzuge die. Der Standardwert ist 0, was bedeutet, dass die Gewichtung für Vermutungsklauseln berechnet wird
wird nicht geändert.

-FullRed
Aktiviert/deaktiviert die vollständige Reduzierung. Wenn auf 0 gesetzt, gilt nur die Menge der abgearbeiteten Klauseln
völlig unterreduziert. Wenn auf 1 gesetzt, werden alle aktuellen Halteklauseln (abgearbeitet und) berücksichtigt
nutzbar) sind vollständig untereinander reduziert. Der Standardwert ist 1.

-FuncWeight
Legt die Gewichtung von Funktions-/Prädikatsymbolen fest. Das Gewicht der Klauseln ist die Summe aller
Symbolgewichte. Dieses Gewicht wird bei der Auswahl der angegebenen Klausel berücksichtigt.
Standard ist 1.

-VarWeight
Legt die Gewichtung variabler Symbole fest (siehe -FuncWeight). Der Standardwert ist 1.

-PrefVar
Aktiviert/deaktiviert die Präferenz für Klauseln mit vielen Variablen. While-Klauseln sind
nach Gewicht ausgewählt, wenn diese Option gesetzt ist und zwei Klauseln das gleiche Gewicht haben, wird die
Eine Klausel mit variableren Vorkommen wird bevorzugt. Der Standardwert ist 0.

-BoundMode
Wählt den Modus für gebundene Einschränkungen aus. Modus 0 bedeutet keine Einschränkung, bei Einstellung 1 alle
Neu generierte Klauseln werden durch Gewichtung (siehe -BoundStart) und wenn auf 2 gesetzt, eingeschränkt
Klauseln sind durch die Tiefe eingeschränkt. Der Standardwert ist 0.

-BoundStart
Die Startbeschränkung des ausgewählten gebundenen Modus. Wenn der gebundene Modus beispielsweise 1 ist und
Wenn der gebundene Start auf 5 gesetzt ist, werden alle Klauseln mit einer Gewichtung größer als 5 gelöscht, bis der
Satz ist gesättigt. Dies führt zu einer Erhöhung des ermittelten verwendeten Grenzwertes
durch die minimale Erhöhung wird eine Vorher gelöschte Klausel gespeichert. Der Standardwert ist -1, was bedeutet, dass keine Grenze vorliegt
Beschränkung.

-BoundLoops
Die Anzahl der Schleifen, die die Aktionseinschränkungen/-erhöhungsgrenzen anwenden. Wenn die Nummer
Wird die Anzahl der Schleifen überschritten, werden alle gebundenen Einschränkungen aufgehoben. Der Standardwert ist 1.

-ApplyDefs
Legt die maximale Anzahl von Anwendungen von Atomdefinitionen auf Eingabeformeln fest.
Der Standardwert ist 0, was bedeutet, dass überhaupt keine Anwendungen vorhanden sind.

-Bestellung
Legt die Termreihenfolge fest. Bei 0 wird KBO ausgewählt, bei 1 wird RPOS ausgewählt. Standard
ist 0.

-CNFQuantExch
Falls festgelegt, werden nicht konstante Skolem-Terme in der Klauselform der Vermutung ersetzt
durch Konstanten. Wird automatisch auf die optimierte Funktionsübersetzung eingestellt
Modal- oder Beschreibungslogikformeln. Der Standardwert ist 0.

-CNFOptSkolem
Aktiviert/deaktiviert die optimierte Skolemisierung. Der Standardwert ist 1.

-CNFStrSkolem
Aktiviert/deaktiviert die starke Skolemisierung. Der Standardwert ist 1.

-CNFProofSteps
Legt die maximale Anzahl von Beweisschritten in einem optimierten Skolemisierungsbeweisversuch fest.
Standard ist 100.

-CNFSub
Aktiviert/deaktiviert die Subsumtion für die von der CNF-Prozedur generierten Klauseln. Standard
ist 1.

-CNFCon
Aktiviert/deaktiviert die Verdichtung der von der CNF-Prozedur generierten Klauseln. Standard ist
1.

-CNFRedTime
Legt die Gesamtzeit in Sekunden fest, die während der CNF für die Reduzierung aufgewendet werden soll
Transformation. Betroffene Reduktionen sind optimierte Skolemisierung, Verdichtung und
Subsumtion. Der Standardwert ist -1, was bedeutet, dass die Reduzierungszeit überhaupt nicht begrenzt ist.

-CNFRenening
Aktiviert/deaktiviert das Umbenennen von Formeln. Bei der Einstellung 1 ist die optimierte Umbenennung aktiviert
minimiert die Anzahl der eventuell generierten Klauseln. Bei der Einstellung 2 erfolgt eine komplexe Umbenennung
aktiviert, das für jede komplexe Formel, also jede, ein neues Skolem-Prädikat einführt
Formel, die kein Literal ist. Wenn die Quantifizierung auf 3 eingestellt ist, ist die Umbenennung aktiviert
führt ein neues Skolem-Prädikat für jede Unterformel ein, die mit einem Quantor beginnt.
Standard ist 1.

-CNFRenMatch
Wenn festgelegt, werden Umbenennungsvarianten-Unterformeln durch dasselbe Skolem-Literal ersetzt. Standard
ist 1.

-CNFPUmbenennung
Aktiviert/deaktiviert das Drucken von Formelumbenennungsanwendungen. Der Standardwert ist 0.

-CNFFEqR
Aktiviert/deaktiviert bestimmte Gleichheitsreduzierungstechniken auf Formelebene. Standard
ist 1.

-IEmS
Aktiviert/deaktiviert die Inferenzregel „Empty Sort“. Der Standardwert ist 0.

-Ist oder
Aktiviert/deaktiviert die Inferenzregel Sortierauflösung. Der Standardwert ist 0.

-IEqR
Aktiviert/deaktiviert die Inferenzregel Gleichheitsauflösung. Der Standardwert ist 0.

-IERR
Aktiviert/deaktiviert die Inferenzregel „Reflexivitätsauflösung“. Der Standardwert ist 0.

-IEqF
Aktiviert/deaktiviert die Inferenzregel Equality Factoring. Der Standardwert ist 0.

-IMPm
Aktiviert/deaktiviert die Inferenzregel Merging Paramodulation. Der Standardwert ist 0.

-ISpR
Aktiviert/deaktiviert die Inferenzregel Superposition Right. Der Standardwert ist 0.

-IOPm
Aktiviert/deaktiviert die Inferenzregel „Geordnete Paramodulation“. Der Standardwert ist 0.

-ISPm
Aktiviert/deaktiviert die Inferenzregel Standardparamodulation. Der Standardwert ist 0.

-ISpL
Aktiviert/deaktiviert die Inferenzregel Superposition Left. Der Standardwert ist 0.

-IORe
Aktiviert/deaktiviert die Inferenzregel „Ordered Resolution“. Wenn auf 1 gesetzt, Bestellt
Die Auflösung ist aktiviert, es werden jedoch keine Auflösungsrückschlüsse mit Gleichungen generiert. Wenn
Bei Einstellung auf 2 werden Gleichungen auch für Ordered Resolution-Schritte berücksichtigt. Standard ist
0.

-ISRe
Aktiviert/deaktiviert die Inferenzregel Standardauflösung. Wenn auf 1 gesetzt, Standard
Die Auflösung ist aktiviert, es werden jedoch keine Auflösungsrückschlüsse mit Gleichungen generiert. Wenn
Bei Einstellung auf 2 werden Gleichungen auch für Standardauflösungsschritte berücksichtigt. Standard ist
0.

-Ich bin schüchtern
Aktiviert/deaktiviert die Inferenzregel Standard Hyper-Resolution. Der Standardwert ist 0.

-IOHy
Aktiviert/deaktiviert die Inferenzregel Ordered Hyper-Resolution. Der Standardwert ist 0.

-IURR
Aktiviert/deaktiviert die Inferenzregel Unit Resulting Resolution. Der Standardwert ist 0.

-IOFc
Aktiviert/deaktiviert die Inferenzregel Ordered Factoring. Wenn auf 1 gesetzt, geordnetes Factoring
ist aktiviert, aber es werden nur Faktorisierungsinferenzen mit positiven Literalen generiert. Wenn festgelegt
Zu 2 werden auch negative Literale für Schlussfolgerungen berücksichtigt. Der Standardwert ist 0.

-ISFc
Aktiviert/deaktiviert die Inferenzregel Standard Factoring. Der Standardwert ist 0.

-IUnR
Aktiviert/deaktiviert die Inferenzregel „Einheitenauflösung“. Der Standardwert ist 0.

-IBUR
Aktiviert/deaktiviert die Inferenzregel „Bounded Depth Unit Resolution“. Der Standardwert ist 0.

-IDEF
Aktiviert/deaktiviert die Inferenzregel „Definitionen anwenden“. Derzeit nicht unterstützt.
Standard ist 0.

-RFRew
Aktiviert/deaktiviert die Reduktionsregel Forward Rewriting. Wenn auf 1 Einheit eingestellt, Neuschreiben und
Nicht-Einheitliches Umschreiben basierend auf einem Subsumptionstest ist aktiviert. Wenn zusätzlich auf 2 gesetzt
Für das Umschreiben von Einheiten und Nicht-Einheiten ist das lokale kontextuelle Umschreiben aktiviert. Wenn auf 3 eingestellt
Zusätzlich zum Umschreiben von Einheiten und Nicht-Einheiten gibt es ein kontextuelles Umschreiben von Unterbegriffen
aktiviert. Untergeordnetes kontextuelles Umschreiben subsumiert lokales kontextuelles Umschreiben. Wenn festgelegt
bis 4 Zusätzlich zu den Umschreibungsregeln von 3 wird auch das kontextuelle Umschreiben von Unterbegriffen getestet
für negative wörtliche Eliminierung. Der Standardwert ist 0.

-RBRew
Aktiviert/deaktiviert die Reduktionsregel „Rückwärtsumschreiben“. Gleiche Werte und Bedeutung wie
für Flag -RFRew, aber in Rückwärtsrichtung verwendet. Der Standardwert ist 0.

-RFMRR
Aktiviert/deaktiviert die Reduktionsregel „Forward Matching Replacement Resolution“. Standard
ist 0.

-RBMRR
Aktiviert/deaktiviert die Reduktionsregel „Backward Matching Replacement Resolution“. Standard
ist 0.

-RObv
Aktiviert/deaktiviert die Reduktionsregel Offensichtliche Reduktion. Der Standardwert ist 0.

-RUNC
Aktiviert/deaktiviert die Reduzierungsregel „Einheitenkonflikt“. Der Standardwert ist 0.

-RTer
Aktiviert/deaktiviert den Terminator, indem die maximale Anzahl von Nicht-Einheitsklauseln festgelegt wird
bei der Suche verwendet werden. Der Standardwert ist 0.

-RTaut
Aktiviert/deaktiviert die Reduktionsregel Tautology Deletion. Wenn auf 1 gesetzt, nur syntaktisch
Tautologien werden erkannt und gelöscht. Wenn auf 2 gesetzt, zusätzlich semantische Tautologien
werden entfernt. Der Standardwert ist 0.

-RSST
Aktiviert/deaktiviert die Reduktionsregel Static Soft Typing. Der Standardwert ist 0.

-RSSi
Aktiviert/deaktiviert die Reduktionsregel Sortiervereinfachung. Der Standardwert ist 0.

-RFSub
Aktiviert/deaktiviert die Reduktionsregel „Forward Subsumption Deletion“. Der Standardwert ist 0.

-RBSub
Aktiviert/deaktiviert die Reduktionsregel „Backward Subsumption Deletion“. Der Standardwert ist 0.

-RAED
Aktiviert/deaktiviert die Reduktionsregel „Zuweisungsgleichung löschen“. Diese Regel wird entfernt
bestimmte Vorkommen von Gleichungen aus Klauseln. Bei der Einstellung 1 beträgt die Reduzierung
garantiert einwandfrei. Bei der Einstellung 2 erfolgt die Reduzierung nur dann, wenn Potenzial vorhanden ist
Das Modell des betrachteten Problems hat einen nichttrivialen Bereich. Der Standardwert ist 0.

-RCon
Aktiviert/deaktiviert die Reduktionsregel Kondensation. Der Standardwert ist 0.

-TDfg2OtterOptions
Aktiviert/deaktiviert die Einbindung eines Otter-Optionsheaders. Diese Option gilt nur für
dfg2otter. Wenn es auf 1 gesetzt ist, enthält es eine Einstellung, die Otter nahezu vollständig macht. Wenn festgelegt
Bei 2 wird der Auto-Modus aktiviert, bei 3 wird der Auto2-Modus aktiviert. Standard ist
0.

-EML
Ein spezielles EML-Flag für Modallogik- oder Beschreibungslogikformeln. Muss nie sein
explizit festlegen. Wird während des Parsens festgelegt.

-EMLAuto
Für den autonomen EML-Modus vorgesehen, noch nicht funktionsfähig. Der Standardwert ist 0.

-EMLÜbersetzung
Bestimmt die Übersetzungsmethode, die für Modallogik- oder Beschreibungslogikformeln verwendet wird.
Wenn auf 0 gesetzt, ist die standardmäßige relationale Übersetzungsmethode (die durch bestimmt wird).
Es wird die übliche Kripke-Semantik verwendet. Wenn auf 1 gesetzt, ist die funktionale Übersetzungsmethode
gebraucht. Bei der Einstellung 2 wird die optimierte funktionale Übersetzungsmethode verwendet. Wenn auf 3 eingestellt,
Es wird die semifunktionale Übersetzungsmethode verwendet. Eine Variation des Optimierten
Die funktionale Übersetzungsmethode wird verwendet, wenn die folgenden Einstellungen angegeben sind:
-EMLTranslation=2 -EMLFuncNary=1. Die Übersetzung erfolgt in Form von n-ary
Prädikate statt unärer Prädikate und Pfade. In der aktuellen Implementierung ist die
Die standardmäßige relationale Übersetzungsmethode ist am allgemeinsten. Es gelten einige Einschränkungen
andere Methoden. Die funktionale Übersetzungsmethode und die semifunktionale Übersetzung
Methoden sind nur für die grundlegende multimodale Logik verfügbar K(m) ggf. mit Seriennummer
(gesamte) Modalitäten (-EMLTheory=1), plus Nominale (ABox-Anweisungen), terminologisch
Axiome und allgemeine Inklusions- und Äquivalenzaxiome. Die optimierte Funktionalität
Übersetzungsmethoden werden nur für implementiert K(m), möglicherweise mit seriellen Modalitäten.
Standard ist 0.

-EML2Rel
Wenn diese Option festgelegt ist, werden Aussagen-/Boolesche Formeln in relationale Formeln konvertiert
bevor sie in die Logik erster Ordnung übersetzt werden. Der Standardwert ist 0.

-EMLTheorie
Legt fest, welche Hintergrundtheorie angenommen wird. Wenn auf 0 gesetzt, lautet die Hintergrundtheorie
leer. Wenn der Wert auf 1 gesetzt ist, wird die Serialität (die Hintergrundtheorie für KD) für alle hinzugefügt
Modalitäten. Wenn der Wert auf 2 gesetzt ist, wird Reflexivität (die Hintergrundtheorie für KT) hinzugefügt
alle Modalitäten. Wenn der Wert auf 3 gesetzt ist, wird Symmetrie (die Hintergrundtheorie für KB) hinzugefügt
für alle Modalitäten. Wenn der Wert auf 4 gesetzt ist, gilt Transitivität (die Hintergrundtheorie für K4).
für alle Modalitäten hinzugefügt. Wenn der Wert auf 5 gesetzt ist, gilt die Euklidizität (die Hintergrundtheorie für
K5) wird für alle Modalitäten hinzugefügt. Wenn auf 6 gesetzt, dann Transitivität und Euklidizität
(die Hintergrundtheorie für S4) wird für alle Modalitäten hinzugefügt. Wenn auf 7 eingestellt, dann
Reflexivität, Transitivität und Euklidizität (die Hintergrundtheorie für S5) werden hinzugefügt
für alle Modalitäten. Der Standardwert ist 0.

-EMLFuncNdeQ
Wenn festgelegt, werden Rautenformeln gemäß tr(dia(phi),s) = nde(s) /\ exist übersetzt
x tr(phi,[sx]) (eine nde/Quantorenformel), ansonsten erfolgt die Übersetzung in
gemäß tr(dia(phi),s) = existiert x nde(s) /\ tr(phi,[sx]) (ein Quantor / nde
Formel). Die Übersetzung für Boxformeln ist dual definiert. Das Setzen dieses Flags ist
Nur sinnvoll, wenn das Flag für die funktionale oder halbfunktionale Übersetzungsmethode ist
eingestellt ist. Der Standardwert ist 1.

-EMLFuncNary
Wenn festgelegt, wird die funktionale Übersetzung in geriffelte Logik verwendet. Das bedeutet n-är
Prädikatssymbole werden anstelle von unären Prädikatssymbolen und Pfaden verwendet. Dies einstellen
Flag ist nur zum Testen der lokalen Erfüllbarkeit/Gültigkeit in multimodalem K von Bedeutung.
Standard ist 0.

-EMLFFSorten
Wenn festgelegt, werden Sortierungen nach Begriffen verwendet. Der Standardwert ist 0.

-EMLElimComp
Wenn festgelegt, versuchen Sie, die relationale Zusammensetzung in modalen Parametern zu eliminieren. Der Standardwert ist 0.

-EMLPTrans
Wenn festgelegt, wird die Übersetzung von EML in die Logik erster Ordnung dokumentiert. Der Standardwert ist 0.

-TPTP
Wenn gesetzt, erwartet SPASS eine Eingabedatei in TPTP-Syntax. Der Standardwert ist 0.

-rf Wenn gesetzt, löscht SPASS die Eingabedatei vor der Beendigung. Der Standardwert ist 0.

Beispiele:

So führen Sie SPASS für eine einzelne Datei ohne Optionen aus:

SPASS I

So deaktivieren Sie alle SPASS-Ausgaben außer dem Endergebnis:

SPASS -PGiven=0 -PProblem=0 I

ANMERKUNG

Sie können im Eingabeproblem auch Optionen für SPASS angeben. In der DFG-Syntax würden Sie das tun
-

list_of_settings(SPASS).
{*
set_flag(DocProof,1).
*}
Ende_der_Liste.

um das DocProof-Flag zu setzen.

Es gibt drei Arten von Optionen, die Sie in der Eingabe festlegen können:

set_flag( , ).
Setzt ein Flag auf einen Wert. Gültige Flags und Werte werden im Abschnitt OPTIONEN beschrieben.

set_precedence( ).
Legt die Priorität für die aufgelisteten Symbole fest. Die Rangfolge nimmt von links nach ab
rechts, dh das Symbol ganz links hat die höchste Priorität.

Jeder Eintrag in der Liste hat das Formular

SYMBOL | (SYMBOL, GEWICHT [, {l, r, m}])

Mit dem zweiten Formular können Sie Symbolen Gewichtungen (für KBO) oder einen Status (für) zuweisen
RPOS). Der Status ist entweder @t{l} für von links nach rechts, @t{m} für Multiset oder @t{r} für
rechts nach links. Das Gewicht wird als Ganzzahl angegeben.

set_DomPred( ).
Aufgeführtes Prädikat (DomPred für dominantes Prädikat) Symbole werden zunächst entsprechend geordnet
nach ihrer Priorität, nicht nach ihren Argumentlisten. Nur bei Gleichheit
Prädikate werden die Argumente untersucht. Zum Beispiel, wenn wir die Option hinzufügen

set_DomPred(P).

dann in der Klausel

-> R(f(x,y),a), P(x,a).

das Atom P(x,a) ist streng maximal. Von der aufgeführte Prädikate set_DomPred Option sind
nach dem Vorrang verglichen.

set_selection( ).
Legt die Auswahlliste fest, die vom Select-Flag verwendet werden kann (siehe oben).

set_ClauseFormulaRelation( , eine Reihe von
Axiom-Namenszeichenfolgen)).
Diese Liste wird insbesondere von FLOTTER erstellt und ermöglicht SPASS für ein eventuell gefundenes Objekt
Beweis, um die Beziehung zwischen den im Beweis verwendeten Klauseln und der Eingabe zu zeigen
Formeln. Bei Kombination mit der Option DocProof muss für jedes ein Eintrag vorhanden sein
Klauselnummer. Andernfalls wird ein Fehler gemeldet.

set_ClauseFormulaRelation((1,ax2),(2,ax1),(3,ax3,ax1)).

Nutzen Sie FLOTTER online über die Dienste von onworks.net