From 48e2bb8a2082c57840edb860b7a6873776eb5b7e Mon Sep 17 00:00:00 2001 From: Spencer Killen Date: Thu, 25 May 2023 14:37:24 -0600 Subject: [PATCH] Add examples --- AST.py | 10 +++++----- aft.py | 24 ++++++++++++++++-------- document/document.blg | 2 +- document/document.out | 7 +++++++ document/document.tex | 27 ++++++++++++++++++++++++++- knowledge_bases/simple.hmknf | 3 --- knowledge_bases/simple2.hmknf | 4 ---- knowledge_bases/solver1.hmknf | 8 ++++++++ knowledge_bases/solver2.hmknf | 4 ++++ knowledge_bases/solver3.hmknf | 6 ++++++ knowledge_bases/sr1.hmknf | 8 ++++++++ knowledge_bases/sr2.hmknf | 10 ++++++++++ knowledge_bases/sr3.hmknf | 5 +++++ solver.py | 3 ++- util.py | 9 +++++++-- 15 files changed, 105 insertions(+), 25 deletions(-) create mode 100644 document/document.out delete mode 100644 knowledge_bases/simple.hmknf delete mode 100644 knowledge_bases/simple2.hmknf create mode 100644 knowledge_bases/solver1.hmknf create mode 100644 knowledge_bases/solver2.hmknf create mode 100644 knowledge_bases/solver3.hmknf create mode 100644 knowledge_bases/sr1.hmknf create mode 100644 knowledge_bases/sr2.hmknf create mode 100644 knowledge_bases/sr3.hmknf diff --git a/AST.py b/AST.py index 0136f8c..6553497 100644 --- a/AST.py +++ b/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 () - ont = reduce(partial(OBinary, "&"), orules, OConst.TRUE) + orules = (self.visit(orule) for orule in ctx.orule()) if ctx.orule() else (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)) diff --git a/aft.py b/aft.py index 068ffbf..1de8db2 100755 --- a/aft.py +++ b/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]}) - return X + newX = newX.union({rule.head[0]}) + 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: diff --git a/document/document.blg b/document/document.blg index 800e53f..ef9582d 100644 --- a/document/document.blg +++ b/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 diff --git a/document/document.out b/document/document.out new file mode 100644 index 0000000..9cd656d --- /dev/null +++ b/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 diff --git a/document/document.tex b/document/document.tex index f030a5b..3b61632 100644 --- a/document/document.tex +++ b/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 diff --git a/knowledge_bases/simple.hmknf b/knowledge_bases/simple.hmknf deleted file mode 100644 index 0236f7c..0000000 --- a/knowledge_bases/simple.hmknf +++ /dev/null @@ -1,3 +0,0 @@ --b. -a :- not b. -b :- not a. diff --git a/knowledge_bases/simple2.hmknf b/knowledge_bases/simple2.hmknf deleted file mode 100644 index 7e98533..0000000 --- a/knowledge_bases/simple2.hmknf +++ /dev/null @@ -1,4 +0,0 @@ -:- c. -:- b. -:- a. -a. diff --git a/knowledge_bases/solver1.hmknf b/knowledge_bases/solver1.hmknf new file mode 100644 index 0000000..01683aa --- /dev/null +++ b/knowledge_bases/solver1.hmknf @@ -0,0 +1,8 @@ +# Simple two valued model +# oatoms vs katoms + + +(-a | c) & d. + +a :- not b. +c :- c. \ No newline at end of file diff --git a/knowledge_bases/solver2.hmknf b/knowledge_bases/solver2.hmknf new file mode 100644 index 0000000..2610e94 --- /dev/null +++ b/knowledge_bases/solver2.hmknf @@ -0,0 +1,4 @@ +# KB has a WFM and 2, 2-valued models + +a :- not b. +b :- not a. \ No newline at end of file diff --git a/knowledge_bases/solver3.hmknf b/knowledge_bases/solver3.hmknf new file mode 100644 index 0000000..723f823 --- /dev/null +++ b/knowledge_bases/solver3.hmknf @@ -0,0 +1,6 @@ +# KB has no WFM + +-a | -b. + +a :- not b. +b :- not a. diff --git a/knowledge_bases/sr1.hmknf b/knowledge_bases/sr1.hmknf new file mode 100644 index 0000000..3ca2e44 --- /dev/null +++ b/knowledge_bases/sr1.hmknf @@ -0,0 +1,8 @@ +# Interleaved positive inferences with ontology and program + +(a -> b) & (d -> e). + +a. +c :- b. +d :- c. + diff --git a/knowledge_bases/sr2.hmknf b/knowledge_bases/sr2.hmknf new file mode 100644 index 0000000..0662cd3 --- /dev/null +++ b/knowledge_bases/sr2.hmknf @@ -0,0 +1,10 @@ +# Generate some undefined atoms + +a :- not a'. +a' :- not a. + +:- a'. + + +b. +b :- a. \ No newline at end of file diff --git a/knowledge_bases/sr3.hmknf b/knowledge_bases/sr3.hmknf new file mode 100644 index 0000000..2e9e0fb --- /dev/null +++ b/knowledge_bases/sr3.hmknf @@ -0,0 +1,5 @@ +# Ontology collapses "choice" + +-b. +a :- not b. +b :- not a. diff --git a/solver.py b/solver.py index 921a860..d813428 100755 --- a/solver.py +++ b/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(): diff --git a/util.py b/util.py index c3f6a5c..1b2c56f 100644 --- a/util.py +++ b/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):