Refactor to get threaded operations when writing *.tptp and *.tff KBs

README.md

@@ -638,12 +638,11 @@ Default user/pw: admin/admin
 You can use Sigma without being administrator, but you'll have limited use of
 its functionality.
 
-You'll also need to set a few parameters in your config.xml file. If you chose
-user "admin", then your config.xml will need these 2 new lines added.
+You'll also need to set a parameter in your config.xml file. If you chose
+user "admin", then your config.xml will need this line added.
 
 ```xml
   <preference name="dbUser" value="admin" />
-  <preference name="loadFresh" value="false" />
 ```
 
 To handle the account registration feature, you'll need to have an email account and supply the

build.xml

@@ -73,7 +73,7 @@
 
     <property name="impl.title" value="${ant.project.name}"/>
     <property name="product.Name" value="Sigma Knowledge Engineering Environment (${impl.title})"/>
-    <property name="product.version.major" value="1"/>
+    <property name="product.version.major" value="3"/>
     <property name="product.version.minor" value="0"/>
     <property name="product.version.patch" value="0"/>
     <property name="product.Version" value="${product.version.major}.${product.version.minor}.${product.version.patch}"/>
@@ -375,7 +375,7 @@
     <!-- At this point we will assume you have already complied with the
          README.md under the heading "System preparation on Linux." This task
          will take over from the heading "Linux Installation."  -->
-    <target name="install" depends="init" description="Appends .*hrc files, clones Sigma tools, installs WordNetMappings and SUMO to ${sigma.home}/KBs and builds the E and Vampire Theorem provers">
+    <target name="install" depends="init" description="Appends .*shrc files, clones Sigma tools, installs WordNetMappings and SUMO to ${sigma.home}/KBs and builds the E and Vampire Theorem provers">
         <mkdir dir="${git.home}"/>
         <chmod dir="${git.home}" perm="ugo+rw" includes="**/*"/>
         <mkdir dir="${programs.dir}"/>
@@ -391,9 +391,9 @@
         <antcall target="retrieve.E"/>
 
         <!-- Clone the sigma tools -->
-        <antcall target="clone.sumo"/>
-        <antcall target="clone.tptpantlr"/>
         <antcall target="clone.sigmautils"/>
+        <antcall target="clone.tptpantlr"/>
+        <antcall target="clone.sumo"/>
 
         <!-- Copy sumo and WordNet files to ${sigma.home} -->
         <antcall target="copy.sumo.and.wordnet.to.sigma.home"/>
@@ -434,7 +434,7 @@
     </target>
 
     <!-- When the SUMO KB files get updated, do this frequently -->
-    <target name="refresh.KBs" description="Copy updated KBs from SUMO to ~/.sigmakee -> ($SIGMA_HOME)">
+    <target name="refresh.KBs" depends="update.sumo" description="Copy updated KBs from SUMO to ~/.sigmakee -> ($SIGMA_HOME)">
         <mkdir dir="${user.home}/.${web.app.name}"/>
         <chmod dir="${user.home}/.${web.app.name}" perm="ugo+rw" includes="**/*"/>
         <mkdir dir="${user.home}/.${web.app.name}/KBs"/>
@@ -445,14 +445,22 @@
         </copy>
     </target>
 
-    <target name="clone.sumo">
-        <mkdir dir="${kbs.home}"/>
-        <git command="clone" dir="${kbs.home}">
+    <target name="clone.sigmautils">
+        <mkdir dir="${git.home}/SigmaUtils"/>
+        <git command="clone" dir="${git.home}/SigmaUtils">
+            <args>
+                <arg value="--progress"/>
+                <arg value="--verbose"/>
+                <arg value="https://github.com/ontologyportal/SigmaUtils"/>
+                <arg value="${git.home}/SigmaUtils"/>
+            </args>
+        </git>
+    </target>
+    <target name="update.sigmautils">
+        <git command="pull" dir="${git.home}/SigmaUtils">
             <args>
                 <arg value="--progress"/>
                 <arg value="--verbose"/>
-                <arg value="https://github.com/ontologyportal/sumo"/>
-                <arg value="${kbs.home}"/>
             </args>
         </git>
     </target>
@@ -467,14 +475,38 @@
             </args>
         </git>
     </target>
-    <target name="clone.sigmautils">
-        <mkdir dir="${git.home}/SigmaUtils"/>
-        <git command="clone" dir="${git.home}/SigmaUtils">
+    <target name="update.tptpantlr">
+        <git command="pull" dir="${git.home}/TPTP-ANTLR">
+            <args>
+                <arg value="--progress"/>
+                <arg value="--verbose"/>
+            </args>
+        </git>
+    </target>
+    <target name="clone.sumo">
+        <mkdir dir="${kbs.home}"/>
+        <git command="clone" dir="${kbs.home}">
+            <args>
+                <arg value="--progress"/>
+                <arg value="--verbose"/>
+                <arg value="https://github.com/ontologyportal/sumo"/>
+                <arg value="${kbs.home}"/>
+            </args>
+        </git>
+    </target>
+    <target name="update.sumo">
+        <git command="pull" dir="${kbs.home}">
+            <args>
+                <arg value="--progress"/>
+                <arg value="--verbose"/>
+            </args>
+        </git>
+    </target>
+    <target name="update.sigmakee">
+        <git command="pull" dir="${user.dir}">
             <args>
                 <arg value="--progress"/>
                 <arg value="--verbose"/>
-                <arg value="https://github.com/ontologyportal/SigmaUtils"/>
-                <arg value="${git.home}/SigmaUtils"/>
             </args>
         </git>
     </target>
@@ -497,14 +529,6 @@
             </args>
         </git>
     </target>
-    <target name="update.sigmakee">
-        <git command="pull" dir="${user.dir}">
-            <args>
-                <arg value="--progress"/>
-                <arg value="--verbose"/>
-            </args>
-        </git>
-    </target>
 
     <!-- git macro utils setup from: https://tonyyan.wordpress.com/2017/03/10/integrate-git-into-ant-targets/-->
     <macrodef name="git">

docker/sigma-ci/Dockerfile

@@ -35,6 +35,7 @@ RUN apt-get update && apt-get install -y --install-recommends \
     cp build/vampire vampire ;\
     ./checks/sanity vampire
 
+# For a specific version of Vampire and z3
 #RUN apt update && apt install -y --install-recommends \
 #    build-essential \
 #    clang \
@@ -69,6 +70,12 @@ RUN apt-get update && apt-get install -y --install-recommends \
 # runtime image.
 FROM tomcat:9.0.97-jdk21-temurin-jammy AS runtime
 
+RUN apt-get update && apt-get install -y --no-install-recommends \
+    ant \
+    ant-optional \
+    git \
+    graphviz
+
 COPY --from=builder \
     /usr/local/tomcat/E/PROVER/e_ltb_runner /usr/local/bin/e_ltb_runner
 
@@ -87,8 +94,4 @@ COPY --from=builder \
 COPY --from=builder \
     /usr/local/tomcat/vampire/z3/build/libz3.* /usr/local/bin/
 
-RUN apt-get update && apt-get install -y --no-install-recommends \
-    ant \
-    ant-optional \
-    git \
-    graphviz
+ENV LD_LIBRARY_PATH=/usr/local/bin:$LD_LIBRARY_PATH

nbproject/build.properties

@@ -66,7 +66,6 @@ javadoc.splitindex=true
 javadoc.use=true
 javadoc.version=false
 javadoc.windowtitle=
-#main.class=com.articulate.sigma.KB
 #manifest.mf=MANIFEST.MF
 platform.active=default_platform
 run.classpath=\
@@ -83,6 +82,7 @@ run.classpath=\
 # You may also define separate properties like run-sys-prop.name=value instead of -Dname=value.
 # To set system properties for unit tests define test-sys-prop.name=value:
 #run.jvmargs=-Xmx10g -Xss1m
+debug.jvmargs=-Xmx15g -Xss4m
 run.modulepath=\
     ${javac.modulepath}
 run.test.classpath=\
@@ -101,7 +101,7 @@ source.encoding=UTF-8
 
 # Specific SigmaKEE props
 #app.name=sigma
-#web.app.name=${web.app.name}kee
+#web.app.name=${app.name}kee
 ontologyportal.git=${workspace}
 #web.dir=web
 sigma_src=${basedir}
@@ -125,9 +125,40 @@ kbs_home=../sumo
 #spec.vendor=Adam Pease
 project.license=LICENSE
 
+# Can't override immutable props
+#main.class=com.articulate.sigma.KB
+#run.class=com.articulate.sigma.KButilities
+run.class=${main.class}
+
 # Various runtime arguments here
-#run.args=-g Transitway subclass
-run.args=-t
+
+# Intentional empty arguments
+#run.args=
+
+# Default run for the KB
+#run.args=-c Object Transaction
+
+# Load KB files w/ KButilities (should regenerate the KB if cleaned). -R for
+# rapid (threaded) processing
+run.args=-l -R
+
+# Run Vampire on SUMO.tptp and output proof
+#run.args=-p
+
+# KB, KIF, TPTP3ProofProcessor, TPTPutil, SUMOtoTFAform - run a test
+#run.args=-t
+
+# Formula check for errors
+formula='(=> (and (muscleInsertion ?MC ?BPC) (instance ?H Human) (attribute ?H Healthy)) (exists (?M ?BP) (and (instance ?M ?MC) (instance ?BP ?BPC) (part ?M ?H) (part ?BP ?H) (connects ?M ?BP))))'
+
+# Error checking a formula w/ com.articulate.sigma.KButilities
+#run.args=-v ${formula}
+
+# Translate KB to TFF
+# run com.articulate.sigma.trans.SUMOKBtoTFAKB
+
+# Translate KB to FOF
+# run com.articulate.sigma.trans.SUMOKBtoTPTPKB
 
 # Tomcat Manager properties
 catalina.ops=-Xmx10g -Xss1m
@@ -163,6 +194,15 @@ test.integration.resources.dir=${test.integration.dir}/resources
 #unit.test.suite=com.articulate.sigma.UnitTestSuite
 #integration.test.suite=com.articulate.sigma.IntegrationTestSuite
 
+# Vampire
+
+# default timeout is 60 if -t is not specified
+# NOTE: [- -mode casc] is a shortcut for [- -mode portfolio -sched casc -p tptp]
+tptp.file=${workspace}/sigmakee/nbproject/private/resources/SUMO/SUMO.tptp
+#tptp.file=${sigma_home}/KBs/SUMO.tptp
+vamp.out=${sigma_home}/KBs/vamp-out.txt
+vamp.args=--mode casc -t 900 ${tptp.file} &> ${vamp.out}
+
 #System.out.println("PasswordService: ");
 #System.out.println("-h    show this Help message");
 #System.out.println("-l    Login");