Add examples

AST.py

@@ -31,9 +31,9 @@ class LRule:
     nbody: tuple[atom, ...]
 
     def text(self):
-        head = ",".join(self.head)
+        head = ", ".join(self.head)
         nbody = tuple(f"not {atom}" for atom in self.nbody)
-        body = ",".join(self.pbody + nbody)
+        body = ", ".join(self.pbody + nbody)
         return f"{head} :- {body}."
 
 
@@ -62,7 +62,7 @@ class OBinary(OFormula):
     right: OFormula
 
     def text(self):
-        return f"{self.left.text()} {self.operator} {self.right.text()}"
+        return f"({self.left.text()} {self.operator} {self.right.text()})"
 
 
 @dataclass
@@ -100,8 +100,8 @@ class HMKNFVisitor(ParseTreeVisitor):
         self.oatoms = set()
 
     def visitKb(self, ctx: HMKNFParser.KbContext):
-        orules = (self.visit(orule) for orule in ctx.orule()) if ctx.orule() else ()
+        orules = (self.visit(orule) for orule in ctx.orule()) if ctx.orule() else (OConst.TRUE,)
-        ont = reduce(partial(OBinary, "&"), orules, OConst.TRUE)
+        ont = reduce(partial(OBinary, "&"), orules)
         lrules = tuple(self.visit(lrule) for lrule in ctx.lrule())
         return KB(ont, lrules, Set(self.katoms), Set(self.oatoms))
 

aft.py

@@ -10,7 +10,7 @@ usage: python aft.py < knowledge_bases/simple.hmknf
 from sys import stdin, flags, argv
 from AST import KB, Set, atom, loadProgram
 from hmknf import objective_knowledge
-from util import printp
+from util import format_set, printp, textp
 
 Kinterp = tuple[Set[atom], Set[atom]]
 
@@ -21,14 +21,14 @@ def add_immediate_XY(kb: KB, X: Set[atom], Y: Set[atom]) -> Set[atom]:
     When they are flipped, i.e. X = P, and Y = T, then it computes what is "possibly true"
     This function is monotone w.r.t. the precision ordering
     """
-    _, X, _ = objective_knowledge(kb, X, Set())
+    _, newX, _ = objective_knowledge(kb, X, Set())
     for rule in kb.rules:
         if not X.issuperset(rule.pbody):
             continue
         if Y.intersection(rule.nbody):
             continue
-        X = X.union({rule.head[0]})
+        newX = newX.union({rule.head[0]})
-    return X
+    return newX
 
 
 def extract_OBT_entails_false(kb: KB, T: Set[atom]):
@@ -59,11 +59,15 @@ def fixpoint(op, initial):
     return prev
 
 
-def stable_revision(kb: KB, T: Set[atom], P: Set[atom]):
+def stable_revision(kb: KB, T: Set[atom], P: Set[atom], debug=False):
     def left(T):
+        if debug:
+            print("left:", format_set(T))
         return add_immediate_XY(kb, T, P)
 
     def right(P):
+        if debug:
+            print("right:", format_set(P))
         return add_immediate_XY(kb, P, T) - extract_OBT_entails_false(kb, T)
 
     return (
@@ -73,9 +77,14 @@ def stable_revision(kb: KB, T: Set[atom], P: Set[atom]):
 
 
 def stable_revision_extend(kb: KB, initialT: Set[atom], initialP: Set[atom]):
+    i = -1
+
     def stable_revision_tuple(TP: Kinterp) -> Kinterp:
+        nonlocal i
+        i += 1
         T, P = TP
-        return stable_revision(kb, T, P)
+        print(f"{i}:", textp(T, P))
+        return stable_revision(kb, T, P, True)
 
     return fixpoint(stable_revision_tuple, (initialT, initialP))
 
@@ -83,7 +92,6 @@ def stable_revision_extend(kb: KB, initialT: Set[atom], initialP: Set[atom]):
 def least_stable_fixedpoint(kb: KB):
     return stable_revision_extend(kb, Set(), kb.katoms)
 
-
 def main():
     """"""
     if len(argv) > 1:
@@ -92,7 +100,7 @@ def main():
         in_file = stdin
     kb = loadProgram(in_file.read())
     T, P = least_stable_fixedpoint(kb)
-    printp(T, P)
+    print("fixpoint:", textp(T, P))
 
 
 if __name__ == "__main__" and not flags.interactive:

document/document.blg

@@ -1,4 +1,4 @@
-This is BibTeX, Version 0.99d (TeX Live 2022/dev/Debian)
+This is BibTeX, Version 0.99d (TeX Live 2022/Debian)
 Capacity: max_strings=200000, hash_size=200000, hash_prime=170003
 The top-level auxiliary file: document.aux
 The style file: plain.bst

document/document.out

@@ -0,0 +1,7 @@
+\BOOKMARK [1][-]{section.1}{\376\377\000A\000n\000\040\000A\000p\000p\000r\000o\000x\000i\000m\000a\000t\000o\000r\000\040\000H\000y\000b\000r\000i\000d\000\040\000M\000K\000N\000F\000\040\000k\000n\000o\000w\000l\000e\000d\000g\000e\000\040\000b\000a\000s\000e\000s}{}% 1
+\BOOKMARK [1][-]{appendix.A}{\376\377\000L\000a\000t\000t\000i\000c\000e\000\040\000T\000h\000e\000o\000r\000y}{}% 2
+\BOOKMARK [1][-]{appendix.B}{\376\377\000P\000a\000r\000t\000i\000a\000l\000\040\000S\000t\000a\000b\000l\000e\000\040\000M\000o\000d\000e\000l\000\040\000S\000e\000m\000a\000n\000t\000i\000c\000s}{}% 3
+\BOOKMARK [2][-]{subsection.B.1}{\376\377\000F\000i\000x\000p\000o\000i\000n\000t\000\040\000O\000p\000e\000r\000a\000t\000o\000r\000s}{appendix.B}% 4
+\BOOKMARK [1][-]{appendix.C}{\376\377\000A\000p\000p\000r\000o\000x\000i\000m\000a\000t\000i\000o\000n\000\040\000F\000i\000x\000p\000o\000i\000n\000t\000\040\000T\000h\000e\000o\000r\000y}{}% 5
+\BOOKMARK [1][-]{appendix.D}{\376\377\000H\000y\000b\000r\000i\000d\000\040\000M\000K\000N\000F\000\040\000K\000n\000o\000w\000l\000e\000d\000g\000e\000\040\000B\000a\000s\000e\000s}{}% 6
+\BOOKMARK [2][-]{subsection.D.1}{\376\377\000A\000n\000\040\000E\000x\000a\000m\000p\000l\000e\000\040\000K\000n\000o\000w\000l\000e\000d\000g\000e\000\040\000B\000a\000s\000e}{appendix.D}% 7

document/document.tex

@@ -1,6 +1,7 @@
 \documentclass{article}
 
 \usepackage{natbib}
+\usepackage{hyperref}
 
 \input{common}
 
@@ -14,6 +15,20 @@
 
 \section{An Approximator Hybrid MKNF knowledge bases}
 
+A program $\P$ is a set of (normal) rules. An ontology $\OO$ is a first-order formula.
+\begin{definition}
+    Given a set of atoms $S$ and an atom $a$. We use $\OBO{S}$ to denote the first-order formula obtained by extending $\OO$ with every atom from $S$ fixed to be true. The relation
+    \begin{align*}
+        \OBO{S} \models a
+    \end{align*}
+    Holds if either 
+    \begin{itemize}
+        \item there is no satisfying assignment for $\OBO{S}$ (The principle of explosion)
+        \item for every satisfying assignment for $\OBO{S}$, $a$ is true, $\OBO{S}$ is logically equivalent to $\OBO{S \union \{ a\}}$
+    \end{itemize}   
+    Holds if when we fix every atom in $S$ to be true with 
+\end{definition}
+
 The lattice $\langle \L^2, \preceq_p \rangle$
 
 \begin{align*}
@@ -26,6 +41,16 @@ The lattice $\langle \L^2, \preceq_p \rangle$
     S(\Phi)(T, P) \define \Bigl( \lfp~\Gamma(\cdot, P),~ \lfp\,\Bigl(  \Gamma(\cdot, T) \setminus extract(T) \Bigr) \Bigr)
 \end{align*}
 
+\begin{definition}
+    A (hybrid MKNF) knowledge base $\KB = (\OO, \P)$  is a program $\P$ and an ontology $\OO$\footnote{See \Section{section-prelim-hmknf} for a formal definition}
+    An interpretation $(T, P)$\footnote{See \Section{psms} for definition of interpretations} is an MKNF model of $\KB$ if 
+    \begin{itemize}
+        \item $T \subseteq P$
+        \item $\OBO{P}$ is consistent, i.e.,  $\OBO{P} \not\models \bot$ (It follows that $\OBO{T} \not\models \bot$)
+        \item All the rules are satisfied, $\lfp~{\Gamma(\cdot, T)} = P$.
+    \end{itemize}
+\end{definition}
+
 \appendix
 
 \section{Lattice Theory}
@@ -59,7 +84,7 @@ The lattice $\langle \L^2, \preceq_p \rangle$
 \end{definition}
 
 
-\section{Partial Stable Model Semantics}
+\section{Partial Stable Model Semantics}\label{psms}
 
 \begin{definition}
     A (ground and normal) {\em answer set program} $\P$ is a set of rules where each rule $r$ is of the form

knowledge_bases/simple.hmknf

@@ -1,3 +0,0 @@
--b.
-a :- not b.
-b :- not a.

knowledge_bases/simple2.hmknf

@@ -1,4 +0,0 @@
-:- c.
-:- b.
-:- a.
-a.

knowledge_bases/solver1.hmknf

@@ -0,0 +1,8 @@
+# Simple two valued model
+# oatoms vs katoms
+
+
+(-a | c) & d.
+
+a :- not b.
+c :- c.

knowledge_bases/solver2.hmknf

@@ -0,0 +1,4 @@
+# KB has a WFM and 2, 2-valued models
+
+a :- not b.
+b :- not a.

knowledge_bases/solver3.hmknf

@@ -0,0 +1,6 @@
+# KB has no WFM
+
+-a | -b.
+
+a :- not b.
+b :- not a.

knowledge_bases/sr1.hmknf

@@ -0,0 +1,8 @@
+# Interleaved positive inferences with ontology and program
+
+(a -> b) & (d -> e).
+
+a.
+c :- b.
+d :- c.
+

knowledge_bases/sr2.hmknf

@@ -0,0 +1,10 @@
+# Generate some undefined atoms
+
+a :- not a'.
+a' :- not a.
+
+:- a'.
+
+
+b.
+b :- a.

knowledge_bases/sr3.hmknf

@@ -0,0 +1,5 @@
+# Ontology collapses "choice"
+
+-b.
+a :- not b.
+b :- not a.

solver.py

@@ -14,6 +14,7 @@ from more_itertools import peekable
 
 from AST import loadProgram, atom, Set, KB
 from aft import Kinterp, add_immediate_XY, fixpoint, stable_revision
+from hmknf import oformula_sat
 from util import printp, powerset
 
 
@@ -34,7 +35,7 @@ def verify(kb: KB, T: Set[atom], P: Set[atom]) -> bool:
     def check_rules(P: Set[atom]):
         return add_immediate_XY(kb, P, T)
 
-    return fixpoint(check_rules, Set()) == P
+    return oformula_sat(kb.ont, P) and fixpoint(check_rules, Set()) == P
 
 
 def main():

util.py

@@ -2,6 +2,7 @@ from functools import wraps
 from AST import Set, atom
 import more_itertools
 
+
 def powerset(items):
     return map(Set, more_itertools.powerset(items))
 
@@ -10,12 +11,16 @@ def format_set(s: Set[atom]):
     return "{" + ", ".join(sorted(s)) + "}"
 
 
-def printp(*args):
+def textp(*args):
     whole = "("
     sets = (format_set(arg) for arg in args)
     whole += ", ".join(sets)
     whole += ")"
-    print(whole)
+    return whole
+
+
+def printp(*args):
+    print(textp(*args))
 
 
 def prints_input(*pos):