add check that defaults to HOL embedding if extended specifications a…

…re given that are not supported by the FOL embedding
leoprover · May 22, 2023 · 5c6e103 · 5c6e103
1 parent 13c500b
commit 5c6e103
Show file tree

Hide file tree

Showing 2 changed files with 32 additions and 9 deletions.
diff --git a/README.md b/README.md
@@ -110,8 +110,8 @@ thf(advanced,logic,(
         $quantification == $cumulative,
         $modalities ==
           [ $modal_system_S5,
-            [#a] == $modal_system_KB,
-            [#b] == $modal_system_K ] ] )).
+            {$box(#a)} == $modal_system_KB,
+            {$box(#b)} == $modal_system_K ] ] )).
 ```
 Here box operator a is system KB, box operator b is K. Of course, also lists of axiom schemes can be used. All further modal operators are S5 (if existent).
 

diff --git a/embedding-runtime/src/main/scala/leo/modules/embeddings/ModalEmbedding.scala b/embedding-runtime/src/main/scala/leo/modules/embeddings/ModalEmbedding.scala
@@ -36,13 +36,18 @@ object ModalEmbedding extends Embedding {
       val maybeSpec = getLogicSpecFromProblem(problem.formulas)
       maybeSpec match {
         case Some(spec) if spec.formulaType == TPTP.AnnotatedFormula.FormulaType.TFF =>
-          System.err.println(s"%%% First-order input detected, using modal-logic-to-TFF embedding (redirected from embedding '$$$name' to embedding '${FirstOrderManySortedToTXFEmbedding.name}' version ${FirstOrderManySortedToTXFEmbedding.version}). Use flag -p FORCE_HIGHERORDER if you want to have THF output instead.")
-          /* create new parameter set */
-          var parameters: Set[FirstOrderManySortedToTXFEmbedding.FOMLToTXFEmbeddingParameter.Value] = Set.empty
-          if (embeddingOptions.contains(ModalEmbeddingOption.POLYMORPHIC)) parameters = parameters + FOMLToTXFEmbeddingParameter.POLYMORPHIC
-          if (embeddingOptions.contains(ModalEmbeddingOption.EMPTYDOMAINS)) parameters = parameters + FOMLToTXFEmbeddingParameter.EMPTYDOMAINS
-          if (embeddingOptions.contains(ModalEmbeddingOption.LOCALEXTENSION)) parameters = parameters + FOMLToTXFEmbeddingParameter.LOCALEXTENSION
-          FirstOrderManySortedToTXFEmbedding.apply(problem, parameters)
+          // Fallback to HOL embedding if problem
+          // contains extended specification entries (interaction axioms, meta-axioms, etc....)
+          if (testSpecForExtendedEntries(spec)) new ModalEmbeddingImpl(problem, embeddingOptions).apply()
+          else {
+            System.err.println(s"%%% First-order input detected, using modal-logic-to-TFF embedding (redirected from embedding '$$$name' to embedding '${FirstOrderManySortedToTXFEmbedding.name}' version ${FirstOrderManySortedToTXFEmbedding.version}). Use flag -p FORCE_HIGHERORDER if you want to have THF output instead.")
+            /* create new parameter set */
+            var parameters: Set[FirstOrderManySortedToTXFEmbedding.FOMLToTXFEmbeddingParameter.Value] = Set.empty
+            if (embeddingOptions.contains(ModalEmbeddingOption.POLYMORPHIC)) parameters = parameters + FOMLToTXFEmbeddingParameter.POLYMORPHIC
+            if (embeddingOptions.contains(ModalEmbeddingOption.EMPTYDOMAINS)) parameters = parameters + FOMLToTXFEmbeddingParameter.EMPTYDOMAINS
+            if (embeddingOptions.contains(ModalEmbeddingOption.LOCALEXTENSION)) parameters = parameters + FOMLToTXFEmbeddingParameter.LOCALEXTENSION
+            FirstOrderManySortedToTXFEmbedding.apply(problem, parameters)
+          }
         case _ => new ModalEmbeddingImpl(problem, embeddingOptions).apply()
       }
     }
@@ -1446,4 +1451,22 @@ object ModalEmbedding extends Embedding {
 
   }
 
+  // Check if the logic spec contains interactions or other meta-axioms/-properties.
+  private[this] def testSpecForExtendedEntries(spec: TPTP.AnnotatedFormula): Boolean = {
+    import leo.modules.tptputils.SyntaxTransform.transformAnnotatedFormula
+    val specTHF = transformAnnotatedFormula(TPTP.AnnotatedFormula.FormulaType.THF, spec)
+    var result = false
+    specTHF.formula match {
+      case THF.Logical(THF.BinaryFormula(THF.==, THF.FunctionTerm(name, Seq()), THF.Tuple(spec0))) if Seq("$modal", "$alethic_modal", "$deontic_modal", "$epistemic_modal") contains name =>
+        spec0 foreach {
+          case THF.BinaryFormula(THF.==, THF.FunctionTerm("$modalities", Seq()), rhs) =>
+            val (_, _, mapFormulas, metaAxioms) = parseTHFModalSpecRHS(rhs)
+            if (mapFormulas.nonEmpty || metaAxioms.nonEmpty) result = true
+          case _ => () // NOP
+        }
+        result
+      case _ => false
+    }
+  }
+
 }