@@ -18,18 +18,18 @@ object ModalEmbedding extends Embedding {
18
18
override final def embeddingParameter : ModalEmbeddingOption .type = ModalEmbeddingOption
19
19
20
20
override final def name : String = " modal"
21
- override final def version : String = " 1.4 "
21
+ override final def version : String = " 1.5 "
22
22
23
23
private [this ] final val defaultConstantSpec = " $rigid"
24
- private [this ] final val defaultConsequenceSpec = " $global "
24
+ private [this ] final val defaultQuantificationSpec = " $constant "
25
25
private [this ] final val defaultModalitiesSpec = " $modal_system_K"
26
26
override final def generateSpecification (specs : Map [String , String ]): TPTP .THFAnnotated = {
27
27
import modules .input .TPTPParser .annotatedTHF
28
28
val spec : StringBuilder = new StringBuilder
29
29
spec.append(" thf(logic_spec, logic, (" )
30
30
spec.append(" $modal == [" )
31
31
spec.append(" $constants == " ); spec.append(specs.getOrElse(" $constants" , defaultConstantSpec)); spec.append(" ," )
32
- spec.append(" $consequence == " ); spec.append(specs.getOrElse(" $consequence " , defaultConsequenceSpec )); spec.append(" ," )
32
+ spec.append(" $quantification == " ); spec.append(specs.getOrElse(" $quantification " , defaultQuantificationSpec )); spec.append(" ," )
33
33
spec.append(" $modalities == " ); spec.append(specs.getOrElse(" $modalities" , defaultModalitiesSpec))
34
34
spec.append(" ] ))." )
35
35
annotatedTHF(spec.toString)
@@ -63,10 +63,6 @@ object ModalEmbedding extends Embedding {
63
63
" $less" -> RIGIDITY_RIGID , " $lesseq" -> RIGIDITY_RIGID ,
64
64
" $greater" -> RIGIDITY_RIGID , " $greatereq" -> RIGIDITY_RIGID )
65
65
66
- // private final val CONSEQUENCE_GLOBAL = true
67
- // private final val CONSEQUENCE_LOCAL = false
68
- // private final val CONSEQUENCE = state.createKey[String, Boolean]()
69
-
70
66
private final val DOMAIN_CONSTANT = 0
71
67
private final val DOMAIN_VARYING = 1
72
68
private final val DOMAIN_CUMULATIVE = 2
0 commit comments