FLOTTER - En ligne dans le Cloud

PROGRAMME:

Nom

SPASS - prouveur de théorèmes automatisé pour une logique complète du premier ordre avec égalité

SYNOPSIS

PASS [Options] [fichier d'entrée]

DESCRIPTION

SPASS est un prouveur de théorème automatisé pour la logique du premier ordre triée complète avec une égalité qui
étend la superposition par tris et une règle de fractionnement pour l'analyse des cas. SPASS peut également être
utilisé comme démonstrateur de théorème de logique modale et de logique de description.

OPTIONS

Les options de ligne de commande dans SPASS sont implémentées via des modifications de la ligne de commande GNU
package d'options pour C. Le simple fait de donner l'option définit sa valeur à 1 et signifie activer le
option. Pour désactiver une option, la valeur doit être définie sur 0 en déclarant -Option= 0.
Les options suivantes sont actuellement prises en charge par SPASS :

-auto
Active/désactive le mode automatique où SPASS se configure automatiquement. Les
règles d'inférence/réduction, la technologie de tri, l'ordre et la priorité ainsi que
la stratégie de fractionnement et de sélection est définie. En mode automatique, le SPASS est terminé. Mélange
le mode automatique avec des options définies par l'utilisateur peut détruire l'exhaustivité. La valeur par défaut est 1.

-Stdin
Active/désactive l'entrée dans SPASS via stdin. L'argument fichier est ignoré. La valeur par défaut est 0.

-Interactif
Active/désactive le mode interactif. Tout d'abord, SPASS reçoit un ensemble d'axiomes, puis
le prouveur accepte les tâches de preuve ultérieures. La valeur par défaut est 0.

-Flotteur
Active/désactive le mode de traduction CNF de SPASS. Si l'option est définie, SPASS uniquement
effectue une traduction sous forme normale de clause. Si aucun argument de fichier de sortie n'est donné SPASS
imprime le CNF sur stdout. La valeur par défaut est 0.

-SOS
Active/désactive l'ensemble de la stratégie de support. La valeur par défaut est 0.

-Fentes=n
Définit le nombre d'applications de fractionnement possibles sur n. Si n=-1 alors le nombre de
les divisions ne sont pas limitées. La valeur par défaut est 0.

-Mémoire=n
Définit la quantité de mémoire disponible pour SPASS pour la recherche de preuves à n octets. Les
la mémoire nécessaire au démarrage de SPASS ne peut pas être restreinte. La valeur par défaut est -1, ce qui signifie que
les allocations de mémoire ne sont limitées que par la mémoire disponible.

-TimeLimit=n
Définit une limite de temps pour la recherche de preuves à n secondes. La valeur par défaut est -1, ce qui signifie que SPASS
peut courir pour toujours. La limite de temps est interrogée lorsque SPASS sélectionne une nouvelle clause pour
inférences. Si une seule étape d'inférence provoque une explosion du nombre de
clauses, il peut donc arriver qu'un délai donné soit largement dépassé.

-Doc SST
Active/désactive la sortie de la documentation pour la saisie logicielle statique. La théorie des tris utilisée comme
ainsi que la tentative de preuve (échouée) pour la contrainte de tri est imprimée. La valeur par défaut est 0.

-DocProof
Active/désactive la documentation de la preuve. Si SPASS trouve une épreuve, elle est finalement imprimée.
Si SPASS trouve une saturation, l'ensemble de clauses saturé est finalement imprimé.
L'activation de la documentation de la preuve peut réduire considérablement les performances de SPASS, car
le prouveur doit stocker des clauses qui peuvent être jetées autrement. La valeur par défaut est 0.

-DocSplit
Définit la documentation des étapes de retour en arrière fractionnées. S'il est défini sur 1, le courant
le niveau de retour en arrière est imprimé. S'il est défini sur 2, il s'imprime également en cas de division
revenir en arrière sur la clause de retour en arrière. La valeur par défaut est 0.

-Boucles
Définit le nombre maximal d'itérations de boucle principale pour SPASS. La valeur par défaut est -1.

-PSub
Active/désactive l'impression des clauses subsumées. La valeur par défaut est 0.

-PRew
Active/désactive l'impression des applications de réécriture simples. La valeur par défaut est 0.

-PCon
Active/désactive l'impression des applications de condensation. La valeur par défaut est 0.

-PTaut
Active/désactive l'impression des applications de suppression de tautologie. La valeur par défaut est 0.

-PObv
Active/désactive l'impression des applications de réduction évidentes. La valeur par défaut est 0.

-PSSi
Active/désactive l'impression des applications de simplification de tri. La valeur par défaut est 0.

-PSST
Active/désactive l'impression des applications de saisie logicielle statique. Toutes les clauses supprimées sont
imprimé. La valeur par défaut est 0.

-PMRR
Active/désactive l'impression des applications de résolution de remplacement correspondantes. La valeur par défaut est
0.

-PunC
Active/désactive l'impression des applications en conflit d'unités. La valeur par défaut est 0.

-PAED
Active/désactive l'impression des clauses où les équations redondantes ont été supprimées
(suppression de l'équation d'affectation).

-PDer
Active/désactive l'impression des clauses dérivées des inférences. La valeur par défaut est 0.

-PGiv
Active/désactive l'impression de la clause donnée, sélectionnée pour effectuer des inférences.
La valeur par défaut est 0.

-Étiquettes
Active/désactive l'impression d'étiquettes. Si le -DocProof est défini et aucune étiquette pour
les formules sont fournies par l'entrée, SPASS génère des étiquettes génériques qui sont ensuite
imprimé en activant cette option. La valeur par défaut est 0.

-Pgardé
Active/désactive l'impression des clauses conservées. Ce sont des clauses générées par des inférences
(backtracking) qui ne sont pas redondants. Clauses dérivées lors de la saisie
réduction/saturation ne sont pas imprimées. La valeur par défaut est 0.

-Pproblème
Active/désactive l'impression de l'ensemble de clauses d'entrée. La valeur par défaut est 1.

-PemptyClause
Active/désactive l'impression des clauses vides dérivées. La valeur par défaut est 0.

-PStatistique
Active/désactive l'impression d'une statistique finale sur les clauses dérivées/backtrackées/conservées,
fractionnés effectués, temps utilisé et espace utilisé. La valeur par défaut est 1.

-FPModèle
Active/désactive la sortie d'un modèle éventuellement trouvé dans un fichier. S'il est défini sur 1, tous
les clauses de l'ensemble final sont imprimées. Si défini sur 2, seules les clauses potentiellement productives
sont imprimées, c'est-à-dire des clauses sans littéral négatif sélectionné et un maximum positif
une. Si est le nom du problème d'entrée et le finalement généré
l'ensemble est saturé, la saturation est imprimée dans le fichier .model, pour
sinon à .clauses. Ce dernier cas peut, par exemple, être causé par un temps
limite. La valeur par défaut est 0.

-FPDFGProof
Active/désactive la sortie d'une preuve éventuellement trouvée dans un fichier. Utiliser cette option
nécessite de définir l'option -DocProof. Si est le nom de l'entrée
problème auquel la preuve est imprimée .prf. La valeur par défaut est 0.

-Flags
Active/désactive la sortie de toutes les valeurs d'indicateur. Les paramètres du drapeau sont imprimés au
fin d'une exécution SPASS sous la forme d'une section d'entrée DFG-Syntaxe. La valeur par défaut est 0.

-POptSkolem
Active/désactive la sortie des applications de skolemisation optimisées. La valeur par défaut est 0.

-PSrSkolem
Active/désactive la sortie des applications de skolemisation puissantes. La valeur par défaut est 0.

-PBDC
Active/désactive la sortie des clauses supprimées en raison de restrictions liées. Défaut
est 0.

-PBInc
Active/désactive la sortie des modifications de restriction liées. La valeur par défaut est 0.

-PApplyDefs
Active/désactive l'impression d'extensions de définitions d'atomes. La valeur par défaut est 0.

-Sélectionner
Définit la stratégie de sélection pour SPASS. Si défini sur 0, aucune sélection de littéraux négatifs
est fait. S'il est défini sur une autre valeur, au plus un littéral négatif dans une clause est
choisi. Si défini sur 1 littéral négatif dans les clauses avec plus d'un littéral maximal
sont sélectionnés. Soit un littéral négatif avec un prédicat de la liste de sélection (voir
ci-dessous) est choisi ou si aucun littéral négatif n'est disponible, un littéral négatif avec
le poids maximal est choisi. S'il est défini sur 2, les littéraux négatifs sont toujours sélectionnés. De nouveau,
soit un littéral négatif avec un prédicat de la liste de sélection (voir ci-dessous) est
choisi ou si aucun littéral négatif n'est disponible, un littéral négatif avec un maximum
le poids est choisi. Ce dernier cas se traduit par un comportement de type hyperrésolution ordonné
de résolution ordonnée. S'il est défini sur 3, tout littéral négatif avec un prédicat spécifié par
la liste de sélection (voir ci-dessous) est sélectionnée. La valeur par défaut est 1.

-Rentrée
Active/désactive la réduction de l'ensemble de clauses initial. La valeur par défaut est 1.

-Trier
Détermine les littéraux monadiques qui ont construit la contrainte de tri pour la clause initiale
ensemble. S'il est défini sur 0, aucune contrainte de tri n'est générée. Si défini sur 1, tout monadique négatif
les littéraux avec une variable comme argument forment la contrainte de tri. S'il est défini sur 2, tous
les littéraux monadiques négatifs forment la contrainte de tri. Le réglage -Les tris sur 2 peuvent nuire
l'exhaustivité, puisque les contraintes de tri sont soumises à la stratégie de base et à la statique
dactylographie douce. La valeur par défaut est 1.

-Entrée Sat
Active/désactive la saturation d'entrée. La saturation est incomplète mais garantie
mettre fin. La valeur par défaut est 0.

-Rapport WDR
Définit le rapport entre les clauses données sélectionnées en fonction du poids ou de la profondeur dans la recherche
espacer. Le poids est la somme de tous les poids de symboles déterminés par -FuncWeight et
-Options VarWeight. La profondeur de toutes les clauses initiales est 0 et les clauses générées par
les inférences obtiennent la profondeur maximale d'une clause parent plus 1. La valeur par défaut est 5, ce qui signifie
que 4 clauses sont sélectionnées en fonction du poids et la cinquième clause est sélectionnée en fonction de la profondeur.

-PréfCon
Définit le rapport pour calculer le poids des clauses de conjecture et permet donc de
préférez ceux-là. La valeur par défaut est 0, ce qui signifie que le calcul du poids pour les clauses de conjecture
n'est pas modifié.

-PleinRouge
Active/désactive la réduction complète. S'il est défini sur 0, seul l'ensemble des clauses traitées est
complètement inter-réduit. S'il est défini sur 1, toutes les clauses actuellement retenues (traitées et
utilisable) sont complètement inter-réduits. La valeur par défaut est 1.

-FuncWeight
Définit le poids des symboles de fonction/prédicat. Le poids des clauses est la somme de tous
poids des symboles. Ce poids est pris en compte pour la sélection de la clause donnée.
La valeur par défaut est 1.

-VarPoids
Définit le poids des symboles variables (voir -FuncWeight). La valeur par défaut est 1.

-VarPréf
Active/désactive la préférence pour les clauses avec de nombreuses variables. Alors que les clauses sont
sélectionné par poids, si cette option est activée et que deux clauses ont le même poids, le
clause avec plus d'occurrences variables est préférée. La valeur par défaut est 0.

-Mode lié
Sélectionne le mode des restrictions liées. Le mode 0 signifie aucune restriction, s'il est défini sur 1, tous
les clauses nouvellement générées sont restreintes par le poids (voir -BoundStart) et si elles sont définies sur 2
les clauses sont limitées par la profondeur. La valeur par défaut est 0.

-Début lié
La restriction de début du mode lié sélectionné. Par exemple, si le mode lié est 1 et
début lié défini sur 5, toutes les clauses avec un poids supérieur à 5 sont supprimées jusqu'à ce que le
l'ensemble est saturé. Cela provoque une augmentation de la valeur limite utilisée qui est déterminée
par l'augmentation minimale en sauvegardant une clause avant suppression. La valeur par défaut est -1, ce qui signifie aucune limite
restriction.

-Boucles liées
Le nombre de boucles appliquant les restrictions d'actions/limite croissante. Si le nombre
de boucles est dépassé toutes les restrictions liées sont annulées. La valeur par défaut est 1.

-AppliquerDefs
Définit le nombre maximal d'applications de définitions d'atomes aux formules d'entrée.
La valeur par défaut est 0, ce qui signifie aucune application.

-Commande
Définit l'ordre des termes. Si 0 alors KBO est sélectionné, si 1 le RPOS est sélectionné. Défaut
est 0.

-CNFQuantExch
Si défini, les termes Skolem non constants sous la forme clausale de la conjecture sont remplacés
par des constantes. Sera automatiquement paramétré pour la traduction fonctionnelle optimisée de
formules logiques modales ou de description. La valeur par défaut est 0.

-CNFptSkolem
Active/désactive la skolemisation optimisée. La valeur par défaut est 1.

-CNFStrSkolem
Active/désactive la skolemisation forte. La valeur par défaut est 1.

-CNFProofÉtapes
Définit le nombre maximal d'étapes de preuve dans une tentative de preuve de skolemisation optimisée.
La valeur par défaut est 100.

-CNFSub
Active/désactive la subsomption sur les clauses générées par la procédure CNF. Défaut
est 1.

-CNFCon
Active/désactive la condensation sur les clauses générées par la procédure CNF. La valeur par défaut est
1.

-CNFRHeure Rouge
Définit le temps global en secondes à consacrer à la réduction pendant le CNF
transformation. Les réductions affectées sont optimisées Skolemisation, condensation et
subsomption. La valeur par défaut est -1, ce qui signifie que le temps de réduction n'est pas du tout limité.

-CNFRnommage
Active/désactive le renommage des formules. Si défini sur 1, le renommage optimisé est activé qui
minimise le nombre de clauses éventuellement générées. Si défini sur 2, le renommage complexe est
activé qui introduit un nouveau prédicat Skolem pour chaque formule complexe, c'est-à-dire tout
formule qui n'est pas un littéral. Si défini sur 3, le renommage de la quantification est activé
introduit un nouveau prédicat Skolem pour chaque sous-formule commençant par un quantificateur.
La valeur par défaut est 1.

-CNFRenMatch
Si défini, les sous-formules de variante de renommage sont remplacées par le même littéral Skolem. Défaut
est 1.

-CNFPRenommer
Active/désactive l'impression des applications de changement de nom de formule. La valeur par défaut est 0.

-CNFEqR
Active/désactive certaines techniques de réduction d'égalité au niveau de la formule. Défaut
est 1.

-IEmS
Active/désactive la règle d'inférence Tri vide. La valeur par défaut est 0.

-ISOR
Active/désactive la règle d'inférence Sort Resolution. La valeur par défaut est 0.

-IEqR
Active/désactive la règle d'inférence Résolution d'égalité. La valeur par défaut est 0.

-IERR
Active/désactive la règle d'inférence Résolution de réflexivité. La valeur par défaut est 0.

-IEqF
Active/désactive la règle d'inférence Equality Factoring. La valeur par défaut est 0.

-IMPm
Active/désactive la règle d'inférence Merging Paramodulation. La valeur par défaut est 0.

-ISpR
Active/désactive la règle d'inférence Superposition Right. La valeur par défaut est 0.

-IOPM
Active/désactive la règle d'inférence Paramodulation ordonnée. La valeur par défaut est 0.

-ISPm
Active/désactive la règle d'inférence Paramodulation standard. La valeur par défaut est 0.

-ISpL
Active/désactive la règle d'inférence Superposition à gauche. La valeur par défaut est 0.

-IORe
Active/désactive la règle d'inférence Résolution ordonnée. Si défini sur 1, Commandé
La résolution est activée mais aucune inférence de résolution avec des équations n'est générée. Si
réglé sur 2, les équations sont également prises en compte pour les étapes de résolution ordonnée. La valeur par défaut est
0.

-ISRé
Active/désactive la règle d'inférence Résolution standard. Si défini sur 1, Standard
La résolution est activée mais aucune inférence de résolution avec des équations n'est générée. Si
réglé sur 2, les équations sont également prises en compte pour les étapes de résolution standard. La valeur par défaut est
0.

-Je suis timide
Active/désactive la règle d'inférence Standard Hyper-Résolution. La valeur par défaut est 0.

-IOHy
Active/désactive la règle d'inférence Ordered Hyper-Resolution. La valeur par défaut est 0.

-IURR
Active/désactive la règle d'inférence Résolution résultante de l'unité. La valeur par défaut est 0.

-IOFc
Active/désactive la règle d'inférence Affacturage ordonné. Si défini sur 1, Factorisation ordonnée
est activé, mais seules les inférences de factorisation avec des littéraux positifs sont générées. Si défini
à 2, les littéraux négatifs sont également pris en compte pour les inférences. La valeur par défaut est 0.

-ISFc
Active/désactive la règle d'inférence Standard Factoring. La valeur par défaut est 0.

-IUnR
Active/désactive la règle d'inférence Résolution d'unité. La valeur par défaut est 0.

-IBUR
Active/désactive la règle d'inférence Résolution d'unité de profondeur limitée. La valeur par défaut est 0.

-IDEF
Active/désactive la règle d'inférence Appliquer les définitions. Actuellement non pris en charge.
La valeur par défaut est 0.

-RFRew
Active/désactive la règle de réduction Forward Rewriting. Si réglé sur 1 unité de réécriture et
la réécriture non unitaire basée sur un test de subsomption est activée. Si réglé sur 2 en plus
à la réécriture unitaire et non unitaire la réécriture contextuelle locale est activée. Si réglé sur 3
en plus de la réécriture unitaire et non unitaire, la réécriture contextuelle du sous-terme est
activé. La réécriture contextuelle de sous-terme englobe la réécriture contextuelle locale. Si défini
à 4 en plus des règles de réécriture de 3, la réécriture contextuelle du sous-terme teste également
pour l'élimination littérale négative. La valeur par défaut est 0.

-RBRew
Active/désactive la règle de réduction Backward Rewriting. Mêmes valeurs et même sens que
pour l'indicateur -RFRew mais utilisé dans le sens inverse. La valeur par défaut est 0.

-RFMRR
Active/désactive la règle de réduction Forward Matching Replacement Resolution. Défaut
est 0.

-RBMRR
Active/désactive la règle de réduction Résolution de remplacement de correspondance descendante. Défaut
est 0.

-RObv
Active/désactive la règle de réduction Réduction évidente. La valeur par défaut est 0.

-RunC
Active/désactive la règle de réduction Conflit d'unités. La valeur par défaut est 0.

-RTer
Active/désactive le terminateur en définissant le nombre maximal de clauses non unitaires à
être utilisé lors de la recherche. La valeur par défaut est 0.

-RTaut
Active/désactive la règle de réduction Suppression de la tautologie. Si défini sur 1, uniquement syntaxique
les tautologies sont détectées et supprimées. Si défini sur 2, des tautologies sémantiques supplémentaires
sont enlevés. La valeur par défaut est 0.

-RSST
Active/désactive la règle de réduction Static Soft Typing. La valeur par défaut est 0.

-RSSi
Active/désactive la règle de réduction Simplification du tri. La valeur par défaut est 0.

-RFSub
Active/désactive la règle de réduction Suppression de la subsomption avant. La valeur par défaut est 0.

-RBSub
Active/désactive la règle de réduction Suppression de la subsomption arrière. La valeur par défaut est 0.

-RAED
Active/désactive la suppression de l'équation d'affectation de la règle de réduction. Cette règle supprime
occurrences particulières d'équations à partir de clauses. S'il est défini sur 1, la réduction est
garanti d'être sain. S'il est réglé sur 2, la réduction n'est saine que s'il y a un potentiel
modèle du problème considéré a un domaine non trivial. La valeur par défaut est 0.

-RCon
Active/désactive la règle de réduction Condensation. La valeur par défaut est 0.

-TDfg2OtterOptions
Active/désactive l'inclusion d'un en-tête d'options Otter. Cette option ne s'applique qu'aux
dfg2otter. S'il est défini sur 1, il inclut un paramètre qui rend Otter presque complet. Si défini
à 2 il active le mode auto et s'il est réglé à 3 il active le mode auto2. La valeur par défaut est
0.

-EML
Un indicateur EML spécial pour les formules de logique modale ou de logique de description. Jamais besoin d'être
fixé explicitement. Est défini pendant l'analyse.

-EMLAuto
Destiné au mode EML Autonomous, pas encore fonctionnel. La valeur par défaut est 0.

-EMLTraduction
Détermine la méthode de traduction utilisée pour les formules de logique modale ou de logique de description.
S'il est défini sur 0, la méthode de traduction relationnelle standard (qui est déterminée par le
sémantique habituelle de Kripke) est utilisé. S'il est défini sur 1, la méthode de traduction fonctionnelle est
utilisé. S'il est défini sur 2, la méthode de traduction fonctionnelle optimisée est utilisée. Si réglé sur 3,
la méthode de traduction semi-fonctionnelle est utilisée. Une variante de l'optimisé
La méthode de traduction fonctionnelle est utilisée, lorsque les paramètres suivants sont spécifiés :
-EMLTranslation=2 -EMLFuncNary=1. La traduction sera en termes de n-aire
prédicats au lieu de prédicats et de chemins unaires. Dans la mise en œuvre actuelle, le
La méthode de traduction relationnelle standard est la plus générale. Certaines restrictions s'appliquent au
Autres méthodes. La méthode de traduction fonctionnelle et la traduction semi-fonctionnelle
les méthodes ne sont disponibles que pour la logique multimodale de base K(m) éventuellement avec série
modalités (totales) (-EMLTheory=1), plus nominaux (instructions ABox), terminologiques
axiomes et axiomes généraux d'inclusion et d'équivalence. Le fonctionnel optimisé
les méthodes de traduction ne sont implémentées que pour K(m), éventuellement avec des modalités en série.
La valeur par défaut est 0.

-EML2Rel
Si défini, les formules de type propositionnel/booléen sont converties en formules relationnelles
avant qu'ils ne soient traduits en logique du premier ordre. La valeur par défaut est 0.

-EMLThéorie
Détermine quelle théorie de fond est supposée. S'il est défini sur 0, la théorie de fond est
vide. Si défini sur 1, alors la sérialité (la théorie de fond pour KD) est ajoutée pour tous
modalités. S'il est défini sur 2, alors la réflexivité (la théorie de fond pour KT) est ajoutée pour
toutes les modalités. Si défini sur 3, alors la symétrie (la théorie de fond pour KB) est ajoutée
pour toutes les modalités. S'il est défini sur 4, alors la transitivité (la théorie de fond pour K4) est
ajouté pour toutes les modalités. S'il est défini sur 5, alors l'euclidité (la théorie de fond pour
K5) est ajouté pour toutes les modalités. S'il est défini sur 6, alors la transitivité et l'euclidité
(la théorie de fond pour S4) est ajoutée pour toutes les modalités. S'il est défini sur 7, alors
la réflexivité, la transitivité et l'euclidité (la théorie de fond pour S5) sont ajoutées
pour toutes les modalités. La valeur par défaut est 0.

-EMLFuncNdeQ
Si défini, les formules de diamant sont traduites selon tr(dia(phi),s) = nde(s) /\ existe
x tr(phi,[sx]) (une formule nde / quantificateur), sinon la traduction est en
selon tr(dia(phi),s) = existe x nde(s) /\ tr(phi,[sx]) (un quantificateur / nde
formule). La traduction pour les formules de boîte est définie en dualité. Définir ce drapeau est
uniquement significatif lorsque le drapeau pour la méthode de traduction fonctionnelle ou semi-fonctionnelle
est réglé. La valeur par défaut est 1.

-EMLFuncNary
Si elle est définie, la traduction fonctionnelle en logique cannelée est utilisée. Cela signifie n-aire
les symboles de prédicat sont utilisés à la place des symboles et des chemins de prédicat unaires. Définir ce
flag n'a de sens que pour tester la satisfiabilité/validité locale dans K multimodal.
La valeur par défaut est 0.

-EMLFFsorts
Si défini, les tris des termes sont utilisés. La valeur par défaut est 0.

-EMLElimComp
Si défini, essayez d'éliminer la composition relationnelle dans les paramètres modaux. La valeur par défaut est 0.

-EMLPTrans
S'il est défini, la conversion EML en logique de premier ordre est documentée. La valeur par défaut est 0.

-TPTP
S'il est défini, SPASS attend un fichier d'entrée en syntaxe TPTP. La valeur par défaut est 0.

-rf S'il est défini, SPASS supprime le fichier d'entrée avant la fin. La valeur par défaut est 0.

EXEMPLES

Pour exécuter SPASS sur un seul fichier sans options :

SPASS I

Pour désactiver toutes les sorties SPASS à l'exception du résultat final :

SPASS -PGiven=0 -PPproblème=0 I

NOTES

Vous pouvez également spécifier des options pour SPASS dans le problème d'entrée. Dans la syntaxe DFG, vous
utilisé

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

pour définir l'indicateur DocProof.

Il existe trois types d'options que vous pouvez définir dans l'entrée :

set_flag( , ).
Définit un indicateur à une valeur. Les indicateurs et valeurs valides sont décrits dans la section OPTIONS.

set_precedence( ).
Définit la priorité des symboles répertoriés. La priorité est décroissante de gauche à
à droite, c'est-à-dire que le symbole le plus à gauche a la priorité la plus élevée.

Chaque entrée de la liste a la forme

SYMBOLE | (SYMBOLE, POIDS [, {l, r, m}])

Vous pouvez utiliser le deuxième formulaire pour affecter des poids à des symboles (pour KBO) ou à un statut (pour
RPOS). Le statut est soit @t{l} pour de gauche à droite, @t{m} pour multiset, ou @t{r} pour
de droite à gauche. Le poids est donné sous forme d'entier.

set_DomPred( ).
Prédicat répertorié (DomPred pour le prédicat dominant) les symboles sont d'abord ordonnés selon
à leur préséance, et non selon leurs listes d'arguments. Uniquement en cas d'égalité
prédicats, les arguments sont examinés. Par exemple, si nous ajoutons l'option

set_DomPred(P).

puis dans la clause

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

l'atome P(x,une) est strictement maximale. Les prédicats répertoriés par le set_DomPred l'option sont
comparés selon l'antériorité.

set_selection( ).
Définit la liste de sélection qui peut être utilisée par le drapeau Select (voir ci-dessus).

set_ClauseFormulaRelation( , séquence de
chaînes de nom d'axiome)).
Cette liste est notamment fixée par FLOTTER et active SPASS pour un éventuel
preuve pour montrer la relation entre les clauses utilisées dans la preuve et l'entrée
formules. Si combiné avec l'option DocProof, alors il doit y avoir une entrée pour chaque
numéro de clause. Sinon, une erreur est signalée.

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

Utilisez FLOTTER en ligne en utilisant les services onworks.net