From bcc9d79d34bf934caaec8eb430e21debd82899a1 Mon Sep 17 00:00:00 2001 From: Spencer Killen Date: Wed, 24 May 2023 19:05:16 -0600 Subject: [PATCH] init --- .devcontainer/devcontainer.json | 18 + .gitignore | 3 + AST.py | 218 +++++++++ Dockerfile | 31 ++ HMKNF.g4 | 25 + Makefile | 24 + README.md | 8 + aft.py | 99 ++++ document.tex | 254 ++++++++++ document/.gitignore | 7 + document/Makefile | 10 + document/common.tex | 131 ++++++ document/document.blg | 46 ++ document/document.tex | 397 ++++++++++++++++ document/refs.bib | 453 ++++++++++++++++++ grammars/HMKNF.interp | 47 ++ grammars/HMKNF.tokens | 23 + grammars/HMKNFLexer.interp | 56 +++ grammars/HMKNFLexer.py | 84 ++++ grammars/HMKNFLexer.tokens | 23 + grammars/HMKNFParser.py | 806 ++++++++++++++++++++++++++++++++ grammars/HMKNFVisitor.py | 83 ++++ grammars/__init__.py | 0 hmknf.py | 64 +++ knowledge_bases/simple.hmknf | 3 + knowledge_bases/simple2.hmknf | 4 + requirements.txt | 3 + solver.py | 56 +++ util.py | 64 +++ 29 files changed, 3040 insertions(+) create mode 100644 .devcontainer/devcontainer.json create mode 100644 .gitignore create mode 100644 AST.py create mode 100644 Dockerfile create mode 100644 HMKNF.g4 create mode 100644 Makefile create mode 100644 README.md create mode 100755 aft.py create mode 100644 document.tex create mode 100644 document/.gitignore create mode 100644 document/Makefile create mode 100644 document/common.tex create mode 100644 document/document.blg create mode 100644 document/document.tex create mode 100644 document/refs.bib create mode 100644 grammars/HMKNF.interp create mode 100644 grammars/HMKNF.tokens create mode 100644 grammars/HMKNFLexer.interp create mode 100644 grammars/HMKNFLexer.py create mode 100644 grammars/HMKNFLexer.tokens create mode 100644 grammars/HMKNFParser.py create mode 100644 grammars/HMKNFVisitor.py create mode 100644 grammars/__init__.py create mode 100644 hmknf.py create mode 100644 knowledge_bases/simple.hmknf create mode 100644 knowledge_bases/simple2.hmknf create mode 100644 requirements.txt create mode 100755 solver.py create mode 100644 util.py diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json new file mode 100644 index 0000000..d99ee83 --- /dev/null +++ b/.devcontainer/devcontainer.json @@ -0,0 +1,18 @@ +{ + "name": "LaTeX dev container", + "image": "sjkillen/aft-may25-2023", + // "build": { + // "context": "..", + // "dockerfile": "../Dockerfile" + // }, + "customizations": { + "vscode": { + "extensions": [ + "James-Yu.latex-workshop", + "torn4dom4n.latex-support", + "mike-lischke.vscode-antlr4", + "ms-python.python" + ] + } + } +} \ No newline at end of file diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..7ac408e --- /dev/null +++ b/.gitignore @@ -0,0 +1,3 @@ +__pycache__ +.antlr +antlr4.jar diff --git a/AST.py b/AST.py new file mode 100644 index 0000000..0136f8c --- /dev/null +++ b/AST.py @@ -0,0 +1,218 @@ +""" +Parse a knowledge base and generate an AST +Can be run directly with program as standard input to view/debug AST + +usage: python AST.py knowledge_bases/simple.hmknf +OR +usage: python AST.py < knowledge_bases/simple.hmknf +""" + + +from itertools import count, product +from string import ascii_lowercase +from sys import argv, flags, stdin +from antlr4 import ParseTreeVisitor, InputStream, CommonTokenStream +from grammars.HMKNFLexer import HMKNFLexer +from grammars.HMKNFParser import HMKNFParser +from dataclasses import dataclass +from more_itertools import partition +from operator import itemgetter +from functools import reduce, partial +from enum import Enum + +atom = str +Set = frozenset + + +@dataclass +class LRule: + head: tuple[atom, ...] + pbody: tuple[atom, ...] + nbody: tuple[atom, ...] + + def text(self): + head = ",".join(self.head) + nbody = tuple(f"not {atom}" for atom in self.nbody) + body = ",".join(self.pbody + nbody) + return f"{head} :- {body}." + + +@dataclass +class OFormula: + def text(self): + if self is OConst.TRUE: + return "TRUE" + elif self is OConst.FALSE: + return "FALSE" + raise Exception("Unknown text repr") + + +class OConst(Enum): + TRUE = OFormula() + FALSE = OFormula() + + def text(self): + return OFormula.text(self) + + +@dataclass +class OBinary(OFormula): + operator: str + left: OFormula + right: OFormula + + def text(self): + return f"{self.left.text()} {self.operator} {self.right.text()}" + + +@dataclass +class OAtom(OFormula): + name: str + + def text(self): + return self.name + + +@dataclass +class ONegation(OFormula): + of: OFormula + + def text(self): + return f"-{self.of.text()}" + + +@dataclass +class KB: + ont: OFormula + rules: tuple[LRule] + katoms: Set[atom] + oatoms: Set[atom] + + def text(self): + ont = f"{self.ont.text()}.\n" + rules = "\n".join(map(LRule.text, self.rules)) + return ont + rules + + +class HMKNFVisitor(ParseTreeVisitor): + def __init__(self) -> None: + self.katoms = set() + 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) + lrules = tuple(self.visit(lrule) for lrule in ctx.lrule()) + return KB(ont, lrules, Set(self.katoms), Set(self.oatoms)) + + def visitLrule(self, ctx: HMKNFParser.LruleContext): + head = self.visit(ctx.head()) if ctx.head() else () + pbody, nbody = self.visit(ctx.body()) if ctx.body() else ((), ()) + return LRule(head, pbody, nbody) + + def visitHead(self, ctx: HMKNFParser.HeadContext): + heads = tuple(str(atom) for atom in ctx.IDENTIFIER()) + self.katoms.update(heads) + return heads + + def visitBody(self, ctx: HMKNFParser.BodyContext): + nbody, pbody = partition( + itemgetter(1), (self.visit(body_atom) for body_atom in ctx.katom()) + ) + return tuple(tuple(item[0] for item in part) for part in (pbody, nbody)) + + def visitOrule(self, ctx: HMKNFParser.OruleContext): + return self.visit(ctx.oformula()) + + def visitDisjOrConj(self, ctx: HMKNFParser.DisjOrConjContext): + return OBinary( + ctx.operator.text, self.visit(ctx.oformula(0)), self.visit(ctx.oformula(1)) + ) + + def visitParenth(self, ctx: HMKNFParser.ParenthContext): + return self.visit(ctx.oformula()) + + def visitImp(self, ctx: HMKNFParser.ImpContext): + return OBinary("->", self.visit(ctx.oformula(0)), self.visit(ctx.oformula(1))) + + def visitLiteral(self, ctx: HMKNFParser.LiteralContext): + return self.visit(ctx.oatom()) + + def visitKatom(self, ctx: HMKNFParser.KatomContext): + name, sign = self.visit(ctx.patom() if ctx.patom() else ctx.natom()) + self.katoms.add(name) + return name, sign + + def visitOatom(self, ctx: HMKNFParser.OatomContext): + name = str(ctx.IDENTIFIER()) + self.oatoms.add(name) + return OAtom(name) + + def visitPatom(self, ctx: HMKNFParser.PatomContext): + return str(ctx.IDENTIFIER()), True + + def visitNatom(self, ctx: HMKNFParser.NatomContext): + return str(ctx.IDENTIFIER()), False + + def visitNegation(self, ctx: HMKNFParser.NegationContext): + return ONegation(self.visit(ctx.oformula())) + + +def check_syntax_constraints(ast: KB): + for rule in ast.rules: + if len(rule.head) > 1: + raise Exception("No rule may have more than 1 atom in its head") + return ast + + +def unique_atom_namer(prefix: str): + for i in count(1): + for suffix in product(ascii_lowercase, repeat=i): + suffix = "".join(suffix) + yield prefix + suffix + + +def desugar_constraints(ast: KB): + used_names = list() + + def add_name(name: str): + used_names.append(name) + return name + + names = map(add_name, unique_atom_namer("constraint_")) + rules = tuple( + LRule( + (name := next(names),), + rule.pbody, + rule.nbody + (name,), + ) + if not rule.head + else rule + for rule in ast.rules + ) + return KB(ast.ont, rules, ast.katoms.union(used_names), ast.oatoms) + + +def loadProgram(fileContents) -> KB: + input_stream = InputStream(fileContents) + lexer = HMKNFLexer(input_stream) + stream = CommonTokenStream(lexer) + parser = HMKNFParser(stream) + tree = parser.kb() + + visitor = HMKNFVisitor() + ast = visitor.visit(tree) + return desugar_constraints(check_syntax_constraints(ast)) + + +def main(): + if len(argv) > 1: + in_file = open(argv[1], "rt", encoding="utf8") + else: + in_file = stdin + + print(loadProgram(in_file.read()).text()) + + +if __name__ == "__main__" and not flags.interactive: + main() diff --git a/Dockerfile b/Dockerfile new file mode 100644 index 0000000..8d9446f --- /dev/null +++ b/Dockerfile @@ -0,0 +1,31 @@ +FROM sjkillen/miktex +LABEL maintainer="sjkillen@ualberta.ca" + +RUN apt-get -qq update +RUN apt-get -qq install sudo git wget default-jre +RUN apt-get -qq install software-properties-common +RUN add-apt-repository -y ppa:deadsnakes/ppa +RUN apt-get -qq install python3.11 +RUN rm /usr/bin/python3 +RUN ln -sT /usr/bin/python3.11 /usr/bin/python3 +RUN ln -sT /usr/bin/python3.11 /usr/bin/python +RUN cd /tmp && wget https://bootstrap.pypa.io/get-pip.py && python get-pip.py + +ARG USERNAME=user +ARG USER_UID=1000 +ARG USER_GID=$USER_UID + +# Copied from https://code.visualstudio.com/docs/remote/containers-advanced#_adding-a-nonroot-user-to-your-dev-container +# Create the user +RUN groupadd --gid $USER_GID $USERNAME \ + && useradd --uid $USER_UID --gid $USER_GID -m $USERNAME --shell /bin/bash \ + # [Optional] Add sudo support. Omit if you don't need to install software after connecting. + && echo $USERNAME ALL=\(root\) NOPASSWD:ALL > /etc/sudoers.d/$USERNAME \ + && chmod 0440 /etc/sudoers.d/$USERNAME + +RUN chown -R $USERNAME:$USERNAME /miktex + +USER $USERNAME + +COPY requirements.txt /tmp/ +RUN python -m pip install -r /tmp/requirements.txt diff --git a/HMKNF.g4 b/HMKNF.g4 new file mode 100644 index 0000000..abde23a --- /dev/null +++ b/HMKNF.g4 @@ -0,0 +1,25 @@ +grammar HMKNF; + +COMMENT: '#' .*? '\n' -> skip; +WS: [ \n\t\r]+ -> skip; + +kb: (lrule | orule)*; + +lrule: ((head body) | head | body) '.'; +head: IDENTIFIER (',' IDENTIFIER)*; +body: ':-' (katom (',' katom)*)?; + +orule: oformula '.'; +oformula: + '(' oformula ')' # parenth + | oatom # literal + | '-' oformula # negation + | oformula (operator = ('|' | '&')) oformula # disjOrConj + | oformula '->' oformula # imp; + +katom: patom | natom; +oatom: IDENTIFIER; +patom: IDENTIFIER; +natom: 'not' IDENTIFIER; + +IDENTIFIER: [a-z'][A-Za-z0-9'_]*; diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..ff719e6 --- /dev/null +++ b/Makefile @@ -0,0 +1,24 @@ +all: grammars + +.PHONY: grammars +grammars: *.g4 grammars/__init__.py + java -cp "${PWD}/antlr4.jar" org.antlr.v4.Tool -Dlanguage=Python3 $< -no-listener -visitor -o grammars +grammars/__init__.py: antlr4.jar requirements + mkdir -p grammars + touch $@ + +.PHONY: requirements +requirements: + python3 -m pip install -r requirements.txt + +antlr4.jar: + rm -f *.jar + wget https://www.antlr.org/download/antlr-4.10.1-complete.jar + mv *.jar antlr4.jar + +.PHONY: clean +clean: + rm -rf grammars + +.PHONY: test +test: ${TESTS} diff --git a/README.md b/README.md new file mode 100644 index 0000000..f1ed4a8 --- /dev/null +++ b/README.md @@ -0,0 +1,8 @@ +# Approximation Fixpoint Theory x Hybrid MKNF KBs + +- AST.py + - Parse a knowledge base (examples in knowledge_bases) +- aft.py + - A stable revision operator +- solver.py + - A naive, enumerative solver that finds partial stable models \ No newline at end of file diff --git a/aft.py b/aft.py new file mode 100755 index 0000000..068ffbf --- /dev/null +++ b/aft.py @@ -0,0 +1,99 @@ +#!/usr/bin/env python3 +""" +Implements code for stable revision. +When run, will compute the least stable fixedpoint of a knowledge base +usage: python aft.py knowledge_bases/simple.hmknf +OR +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 + +Kinterp = tuple[Set[atom], Set[atom]] + + +def add_immediate_XY(kb: KB, X: Set[atom], Y: Set[atom]) -> Set[atom]: + """ + When X is T and Y is P, will compute the atoms that must be true as a consequence of the rules and the ontology + 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()) + 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 + + +def extract_OBT_entails_false(kb: KB, T: Set[atom]): + """ + Returns the set of atoms that are objectively false w.r.t. T + Function is antitone w.r.t. subset relation + """ + _, _, F = objective_knowledge(kb, T, Set()) + return F + + +def approximator(kb: KB, T: Set[atom], P: Set[atom]) -> Kinterp: + return ( + add_immediate_XY(kb, T, P), + add_immediate_XY(kb, P, T) - extract_OBT_entails_false(kb, T), + ) + + +def fixpoint(op, initial): + """ + Iteratively apply a function beginning with the value initial until a fixpoint is reached + E.g. + op(op(op(initation))) + """ + prev = initial + while (current := op(prev)) != prev: + prev = current + return prev + + +def stable_revision(kb: KB, T: Set[atom], P: Set[atom]): + def left(T): + return add_immediate_XY(kb, T, P) + + def right(P): + return add_immediate_XY(kb, P, T) - extract_OBT_entails_false(kb, T) + + return ( + fixpoint(left, Set()), + fixpoint(right, Set()), + ) + + +def stable_revision_extend(kb: KB, initialT: Set[atom], initialP: Set[atom]): + def stable_revision_tuple(TP: Kinterp) -> Kinterp: + T, P = TP + return stable_revision(kb, T, P) + + return fixpoint(stable_revision_tuple, (initialT, initialP)) + + +def least_stable_fixedpoint(kb: KB): + return stable_revision_extend(kb, Set(), kb.katoms) + + +def main(): + """""" + if len(argv) > 1: + in_file = open(argv[1], "rt", encoding="utf8") + else: + in_file = stdin + kb = loadProgram(in_file.read()) + T, P = least_stable_fixedpoint(kb) + printp(T, P) + + +if __name__ == "__main__" and not flags.interactive: + main() diff --git a/document.tex b/document.tex new file mode 100644 index 0000000..48add82 --- /dev/null +++ b/document.tex @@ -0,0 +1,254 @@ +\documentclass{article} + +\input{common} + +\title{Summary of Important Definitions} +\date{May 11th} + + +\begin{document} + \maketitle + + + + \section{Lattice Theory} + + \begin{definition} + A {\em partial order} $\preceq$ is a relation over a set $S$ such that for every triple of elements $x, y, z \in S$ the following hold + \begin{itemize} + \item (reflexivity) $x \preceq x$ + \item (antisymmetry) $(x \preceq y \land y \preceq x) \implies x = y$ + \item (transitivity) $(x \preceq y \land y \preceq z) \implies (x \preceq z)$ + \end{itemize} + \end{definition} + + + \begin{definition} + Given a partial order $\preceq$ over a set $S$ and a subset $X \subseteq S$, a {\em lower bound} of $X$ (resp.\ an {\em upper bound} of $X$) is an element $x \in S$ (Note that it may be the case that $x \not\in X$) such that + \begin{itemize} + \item $\forall y \in X, \boxed{x} \preceq y$ + \item (resp. $\forall y \in X, \boxed{y} \preceq x$) + \end{itemize} + The {\em greatest lower bound} of a set $X \subseteq S$ (denoted as $\textbf{glb}(X)$) is a unique upperbound of the set of all lowerbounds of $X$. + The {\em least upper bound} of a set $X \subseteq S$ (denoted as $\textbf{lub}(X)$) is a unique lowerbound of the set of all upperbounds of $X$. + In general, $\textbf{lub}(X)$ and $\textbf{glb}(X)$ may not exist. + \end{definition} + + \begin{definition} + A (complete) lattice $\langle \mathcal{L}, \preceq \rangle$ is a set of elements $\mathcal{L}$ and a partial order $\preceq$ over $\mathcal{L}$ such that for any set $S \subseteq \mathcal{L}$ + \begin{itemize} + \item $\textbf{lub}(X)$ and $\textbf{glb}(X)$ exist and are unique. + \end{itemize} + \end{definition} + + \subsection{Fixpoint Operators} + + \begin{definition} + Given a complete lattice $\langle \mathcal{L}, \preceq \rangle$, a fixpoint operator over the lattice is a function $\Phi: \mathcal{L} \rightarrow \mathcal{L}$ that is {\em $\preceq$-monotone} + \begin{itemize} + \item $\Phi$ is $\preceq$-monotone if for all $x, y \in \mathcal{L}$ + \begin{align*} + x \preceq y \implies \Phi(x) \preceq \Phi(y) + \end{align*} + (Note: this does not mean the function is inflationary, i.e., $x \preceq \Phi(x)$ may not hold) + \end{itemize} + A {\em fixpoint} is an element $x \in \mathcal{L}$ s.t. $\Phi(x) = x$. + \end{definition} + + \begin{theorem}[Knaster-Tarski] + The set of all fixpoints of a fixpoint operator $\Phi$ on a complete lattice is itself a complete lattice. The least element of this new lattice exists and is called the least fixpoint (denoted as $\lfp~{\Phi}$) + \end{theorem} + + Some intuitions about lattices + \begin{itemize} + \item The entire lattice has a biggest element $\lub{}(\mathcal{L}) = \top$ and a smallest element $\glb{}(\mathcal{L}) = \bot$ + \item When a lattice has a finite height (or finite domain). The least fixed point of a fixpoint operator can be computed by iteratively applying the fixpoint operator to $\bot$ + \item An operator may return an element that is not comparable to the input, however, after a comparable element is returned (either greater or less than) that comparability and direction are maintained for all subsequent iterations. + \item Further, because $\bot$ is less than all elements in the lattice, it is always the case that $\bot \preceq \Phi(\bot)$ + \end{itemize} + + \section{Partial Stable Model Semantics} + + \begin{definition} + A (ground and normal) {\em answer set program} $\P$ is a set of rules where each rule $r$ is of the form + \begin{align*} + h \leftarrow a_0,~ a_1,~ \dots,~ a_n,~ \Not b_0,~\Not b_1,~\dots,~\Not b_k + \end{align*} + where we define the following shorthand for a rule $r \in \P$ + \begin{align*} + \head(r) &= h\\ + \bodyp(r) &= \{ a_0,~ a_1,~ \dots,~ a_n \}\\ + \bodyn(r) &= \{ b_0,~ b_1,~ \dots,~ b_k \} + \end{align*} + \end{definition} + + \begin{definition} + A two-valued interpretation $I$ of a program $\P$ is a set of atoms that appear in $\P$. + \end{definition} + + \begin{definition} + An interpretation $I$ is a \boxedt{model} of a program $\P$ if for each rule $r \in \P$ + \begin{itemize} + \item If $\bodyp(r) \subseteq I$ and $\bodyn(r) \intersect I = \emptyset$ then $\head(r) \in I$. + \end{itemize} + \end{definition} + + \begin{definition} + An interpretation $I$ is a \boxedt{stable model} of a program $\P$ if $I$ is a model of $\P$ \textbf{and} + for every interpretation $I' \subseteq I$ there exists a rule $r \in \P$ such that + \begin{itemize} + \item $\bodyp(r) \subseteq I'$, $\bodyn(r) \intersect I \not= \emptyset$ (Note that this is $I$ and not $I'$) and $\head(r) \not\in I'$ + \end{itemize} + \end{definition} + + \begin{definition} + A three-valued interpretation $(T, P)$ of a program $\P$ is a pair of sets of atoms such that $T \subseteq P$. + The \boxedt{truth-ordering} respects $\ff < \uu < \tt$ and is defined for two three-valued interpretations $(T, P)$ and $(X, Y)$ as follows. + \begin{align*} + (T, P) \preceq_t (X, Y) \textrm{ iff } T \subseteq X \land P \subseteq Y + \end{align*} + The \boxedt{precision-ordering} respects the partial order $\uu < \tt$, $\uu < \ff$ and is defined for two three-valued interpretations $(T, P)$ and $(X, Y)$ as follows. + \begin{align*} + (T, P) \preceq_p (X, Y) \textrm{ iff } T \subseteq X \land \boxed{Y \subseteq P} + \end{align*} + \end{definition} + + \begin{definition} + A three-valued interpretation $(T, P)$ is a {\em model} of a program $\P$ if for each rule $r \in \P$ + \begin{itemize} + \item $\body(r) \subseteq P \land \bodyn(r) \intersect T = \emptyset$ implies $\head(r) \in P$, and + \item $\body(r) \subseteq T \land \bodyn(r) \intersect P = \emptyset$ implies $\head(r) \in T$. + \end{itemize} + \end{definition} + + \begin{definition} + A three-valued interpretation $(T, P)$ is a {\em stable model} of a program $\P$ if it is a model of $\P$ and if for every three-valued interpretation $(X, Y)$ such that $(X, Y) \preceq_t (T, P)$ there exists a rule $r \in \P$ such that either + \begin{itemize} + \item $\bodyp(r) \subseteq Y \land \bodyn(r) \intersect T = \emptyset$ and $\head(r) \not\in Y$ \textbf{OR} + \item $\bodyp(r) \subseteq X \land \bodyn(r) \intersect P = \emptyset$ and $\head(r) \not\in X$ + \end{itemize} + \end{definition} + + + \section{Approximation Fixpoint Theory} + + We can think of a three-valued interpretation $(T, P)$ as an approximation on the set of true atoms. + $T$ is a lower bound and $P$ is the upper bound. + + \begin{definition} + An {\em approximator} is a fixpoint operator on the complete lattice $\langle \wp(\mathcal{L})^2, \preceq_p \rangle$ (called a bilattice) + \end{definition} + Given a function $f(T, P): S^2 \rightarrow S^2$, we define two separate functions + \begin{align*} + f(\cdot, P)_1:~ &S \rightarrow S\\ + f(T, \cdot)_2:~ &S \rightarrow S + \end{align*} + such that + \begin{align*} + f(T, P) = \Big(&(f(\cdot, P)_1)(T), \\&(f(T, \cdot)_2)(P)\Big) + \end{align*} + + \begin{definition} + Given an approximator $\Phi(T, P)$ the stable revision operator is defined as follows + \begin{align*} + S(T, P) = (\lfp{(\Phi(\cdot, P)_1)},~ \lfp{(\Phi(T, \cdot)_2)}) + \end{align*} + Note: the $\lfp$ is applied to a unary operator, thus it's the least fixpoint of the lattice $\langle \wp(\mathcal{L}), \subseteq \rangle$ whose least element is $\emptyset$. + \end{definition} + + \subsection{An Approximator for Partial Stable Semantics} + + \begin{align*} + \Gamma(T, P) &\define \{ \head(r) ~|~ r \in \P, T \subseteq \bodyp(r), \bodyn(r) \intersect P = \emptyset \}\\ + \Gamma(P, T) &\define \{ \head(r) ~|~ r \in \P, P \subseteq \bodyp(r), \bodyn(r) \intersect T = \emptyset \}\\ + \Phi(T, P) &\define \Bigl( \Gamma(T, P), \Gamma(P, T) \Bigr) + \end{align*} + + Without stable revision where $(T, P) = (\{ a, b \}, \{ a, b \})$ + \begin{align*} + \Phi(T, P) = (\{ a, b \}, \{ a, b \}) \textrm{ (fixpoint reached)} + \end{align*} + With stable revision + \begin{align*} + S(T, P) = (\emptyset, \emptyset) \textrm{ (fixpoint reached)} + \end{align*} + + + \begin{proposition}\label{} + Given a poset $\langle \mathcal{L}, \leq \rangle$, + an operator $o: \mathcal{L} \rightarrow \mathcal{L}$ is $\leq$-monotone iff it is $\geq$-monotone + \end{proposition} + \begin{proof} + ($\Rightarrow$) + Initially, we have $\forall x, y \in \mathcal{L}: x \leq y \implies o(x) \leq o(y)$. + Let $a, b \in \mathcal{L}$ such that $a \geq b$. We have $b \leq a$ and can apply our initial assumption to get $o(b) \leq o(a)$. + This gives us $o(a) \geq o(b)$. + We can generalize to obtain $\forall x, y \in \mathcal{L}: x \geq y \implies o(x) \geq o(y)$. + ($\Leftarrow$) Proof is more or less the same + \end{proof} + + % Let $\leq$ and $\leq_i$ be the orderings over the set $\mathcal{L}^2$ such that for each ${(T, P), (X, Y) \in \mathcal{L}^2}$ + % \begin{align*} + % (a, b) \leq (x, y) &\textit{ iff } a \leq x \textrm{ and } b \leq y\\ + % (a, b) \leq_i (x, y) &\textit{ iff } a \leq x \textrm{ and } \boxed{y} \leq b + % \end{align*} + % \begin{proposition} + % Given a poset $\langle \mathcal{L}^2, \leq \rangle$, an operator $o: \wp(\mathcal{L})^2 \rightarrow \wp(\mathcal{L})^2$ is $\leq$-monotone iff it is $\leq_i$-monotone + % \end{proposition} + % \begin{proof} + % ($\Rightarrow$) Initially, we have ${\forall (x, y), (a, b) \in \mathcal{L}^2: (x, y) \leq (a, b) \implies o(x, y) \leq o(a, b)}$. + % If we rearrange the variables we get + % \begin{align*} + % &\forall x, a \in \mathcal{L}: \forall y, b \in \mathcal{L}:\\ + % &~~~~~(x \leq a \land y \leq b) \implies ((o_1(x, y) \leq o_1(a, b)) \land (o_2(x, y) \leq o_2(a, b))) + % \end{align*} + + + % Let $(u, v), (i, k) \in \mathcal{L}^2$ such that $(u, v) \leq_i (i, k)$. We have $(u, k) \leq (i, v)$. We can apply the initial assumption to obtain + % $o(u, k) \leq o(i, v)$. This is equivalent to + % \begin{align*} + % (o_1(u, k) \leq o_1(i, v)) \land (o_2(u, k) \leq o_2(i, v)) + % \end{align*} + % which can be rewritten as + % \begin{align*} + % (o_1(u, k) \leq o_1(i, v)) \land \boxed{(o_2(i, v)) \leq o_2(u, k))} + % \end{align*} + % \end{proof} + + \begin{proposition} + An operator $A : L^2 \rightarrow L^2$ is symmetric and monotone + with respect to both $\leq_i$ and $\leq$ if and only if there is a monotone operator + $O : L \rightarrow L$ such that for every $x, y \in L, A(x, y) = (O (x), O (y ))$ + \end{proposition} + \begin{proof} + ($\Rightarrow$) + From Proposition 5 and 6 we have for any $x \in L$, $A_1(\cdot, x)$ and $A_1(x, \cdot)$ are monotone and $A_1(x, \cdot)$ is antimonotone. + By Proposition 2, $A_1(x, \cdot)$ is constant, denote this constant as the function $O(x)$. + By the symmetric condition, we have $A_1(x, \cdot) = A_2(\cdot, x)$, thus $A(x, y) = (O(x), O(y))$. It follows from the monotonicity of $A$ that $O$ is monotone. + + ($\Leftarrow$) + Clearly $A$ is symmetric, and $\leq$-monotone (Given that $O$ is $\leq$-monotone). Using proposition 3.1 (above) $O(x)$ is $\geq$-monotone, thus $A$ is $\leq_i$-monotone as well. + \end{proof} + + \section{The Polynomial Heirarchy} + Intuitive definitions of ${\sf NP}$ + \begin{itemize} + \item the class of problems which have algorithms that can verify solutions in polynomial time. + \item A problem that can be solved by reducing it to a SAT expression of the form + \begin{align*} + \exists (a \lor b \lor c) \land (\neg a \lor \neg d \lor c)~\land \cdots + \end{align*} + \item (Alternating turing machine) A problem that is solved by some path of an algorithm that is allowed to branch is parallel + \end{itemize} + Intuitive definitions of ${\sf NP^{NP}}$ a.k.a.\ $\Sigma_2^P$ + \begin{itemize} + \item the class of problems which have algorithms that can verify solutions in ${\sf NP}$ time. + \item A problem that can be solved by reducing it to a SAT expression of the form + \begin{align*} + \exists c,~ \forall a,~ b,~ (a \lor b \lor c) \land (\neg a \lor \neg d \lor c)~\land \cdots + \end{align*} + \item (Alternating Turing machine) A problem that is solved by some path of an algorithm that is allowed to branch in parallel. A branch is allowed to switch to ``ALL'' mode only once and require that all subsequent forks return success + \end{itemize} + + +\end{document} \ No newline at end of file diff --git a/document/.gitignore b/document/.gitignore new file mode 100644 index 0000000..b798d48 --- /dev/null +++ b/document/.gitignore @@ -0,0 +1,7 @@ +*.aux +*.fdb_latexmk +*.fls +*.log +*.pdf +*.synctex.gz +*.bbl \ No newline at end of file diff --git a/document/Makefile b/document/Makefile new file mode 100644 index 0000000..19f9ab2 --- /dev/null +++ b/document/Makefile @@ -0,0 +1,10 @@ +all: document.pdf + +%.pdf: %.tex + latexmk -pdf $< + +clean: + ${RM} document.pdf + ${RM} *.bbl + ${RM} *.blg + latexmk -C diff --git a/document/common.tex b/document/common.tex new file mode 100644 index 0000000..ee122e2 --- /dev/null +++ b/document/common.tex @@ -0,0 +1,131 @@ +\usepackage{amsmath} +\usepackage{amsfonts} +\usepackage{amssymb} +\usepackage{amsthm} +\usepackage{graphicx} +\usepackage{float} +\usepackage{verbatim} +\usepackage{enumerate} +\usepackage{mathtools} +\usepackage{accents} +\usepackage{bm}% boldmath + +\usepackage[acronym,hyperfirst=false]{glossaries} + +\newtheorem{theorem}{Theorem}[section] +\newtheorem{proposition}{Proposition}[section] +\newtheorem{example}{Example} +\newtheorem{lemma}{Lemma}[section] +\newtheorem{corollary}[theorem]{Corollary} +\newtheorem{definition}{Definition}[section] +\newtheorem{remark}{Remark} + +\newcommand{\Definition}[1]{Definition~\ref{#1}} +\newcommand{\Section}[1]{Section~\ref{#1}} +\newcommand{\Chapter}[1]{Chapter~\ref{#1}} +\newcommand{\Theorem}[1]{Theorem~\ref{#1}} +\newcommand{\Proposition}[1]{Proposition~\ref{#1}} +\newcommand{\Example}[1]{Example~\ref{#1}} +\newcommand{\Lemma}[1]{Lemma~\ref{#1}} +\newcommand{\Figure}[1]{Figure~\ref{#1}} +\newcommand{\Corollary}[1]{Corollary~\ref{ #1}} +\newcommand{\Remark}[1]{Remark~\ref{#1}} +\newcommand{\Algorithm}[1]{Algorithm~\ref{#1}} +\newcommand{\Line}[1]{line~\ref{#1}} + +\renewcommand{\P}{\mathcal{P}} +\newcommand{\Not}{\textrm{\bf not\,}} +\newcommand{\head}{head} +\newcommand{\intersect}{\cap} +\newcommand{\union}{\cup} +\newcommand{\atoms}{Atoms} +\newcommand{\bodyp}{body^{+}} +\newcommand{\bodyn}{body^{-}} +\newcommand{\body}{body} +\newcommand{\op}[1]{\textbf{#1}} +\newcommand{\pmodels}{\models} + +\newcommand{\KB}{\mathcal{K}} +\newcommand{\bfK}{\textit{\em \textbf{K}}} +\renewcommand{\O}{\mathcal{O}} +\renewcommand{\P}{\mathcal{P}} +\newcommand{\KAK}{\textbf{KA}(\KB)} +\newcommand{\Katom}{\textbf{K}-atom~} +\newcommand{\Katoms}{\textbf{K}-atoms~} +\newcommand{\comp}[1]{\overline{#1}} + +\newcommand{\A}{\textbf{A}} +\newcommand{\T}{\textbf{T}} +\newcommand{\F}{\textbf{F}} + +\newcommand{\boldK}{\bf {K}} +\newcommand{\PP}{\mathcal{x}_{\KBB}} +\newcommand{\M}{\mathcal{M}} +\newcommand{\Ma}{M_0} +\newcommand{\Mb}{M_1} +\newcommand{\MM}{\langle M, M_1 \rangle} +\newcommand{\N}{\mathcal{N}} +\newcommand{\Na}{N_0} +\newcommand{\Nb}{N_1} +\newcommand{\NN}{\langle N, N_1 \rangle} +\newcommand{\MN}{\langle M, N \rangle} +\newcommand{\ff}{{\bf f}} +\newcommand{\uu}{{\bf u}} +\renewcommand{\tt}{{\bf t}} +\newcommand{\mneval}[1]{(I, \MN, \MN)( #1 )} +\newcommand{\meval}[1]{\mneval{#1}} +\newcommand{\mmeval}[1]{\mneval{#1}} +\newcommand{\KBA}{\textsf{KA}} +\newcommand{\OO}{\mathcal{O}} +\newcommand{\OBO}[1]{{{\sf OB}_{\OO,#1}}} +\renewcommand{\P}{\mathcal{P}} +\newcommand{\Q}{\mathcal{Q}} +\newcommand{\Pcomp}{\P_{\textrm{\tiny COMP}}} +\newcommand{\Ploop}{\P_{\textrm{\tiny LOOP}}} +\newcommand{\Atoms}{Atoms} +\newcommand{\Loops}{Loops} +\renewcommand{\implies}{\supset} +\renewcommand{\impliedby}{\subset} +\newcommand{\Rule}{rule} +\newcommand{\eval}[2]{#1\big\{#2\big\}} +\newcommand{\lub}[1]{{\bf lub_{#1}~}} +\newcommand{\glb}[1]{{\bf glb_{#1}~}} +\newcommand{\lfp}{{\bf lfp}} +\newcommand{\fix}[1]{{\bf broken} ~{#1}} +\newcommand{\fixpoints}{\textbf{fixpoints}} + +% https://tex.stackexchange.com/questions/118240/how-to-draw-a-border-around-character-in-a-formula +\makeatletter +\renewcommand{\boxed}[1]{\text{\fboxsep=.2em\fbox{\m@th$\displaystyle#1$}}} +\makeatother +\newcommand{\boxedt}[1]{\boxed{\textrm{#1}}} + +\newcommand{\argblank}{\underline{\hspace{.3cm}}} +\renewcommand{\L}{\mathcal{L}} +\newcommand{\squnion}{\sqcup} +\renewcommand{\implies}{\Rightarrow} +\newcommand{\define}{\coloneqq} +\newcommand{\lcomp}[1]{{#1}^{\mathbf{\hspace{.075em}c}}} + +\newcommand{\noncompare}{\bowtie} +% https://tex.stackexchange.com/questions/378087 +\makeatletter +\newcommand\ineq{}% for safety +\DeclareRobustCommand{\ineq}{\mathrel{\mathpalette\rance@ineq\relax}} +\newcommand{\rance@ineq}[2]{% + \vcenter{\hbox{% + $\m@th#1\mkern1.5mu\underline{\mkern-1.5mu\bowtie\mkern-1.5mu}\mkern1.5mu$% + }}% +} +\makeatother +\newcommand{\noncompareeq}{\ineq} + + + + +\newcommand{\omax}{\textbf{max}} +\newcommand{\omin}{\textbf{min}} + +\newcommand{\project}[2]{\Pi_{#1}(#2)} + +\newcommand{\mknfmodels}{\models_{\mbox{\tiny{\sf MKNF}}}} \ No newline at end of file diff --git a/document/document.blg b/document/document.blg new file mode 100644 index 0000000..800e53f --- /dev/null +++ b/document/document.blg @@ -0,0 +1,46 @@ +This is BibTeX, Version 0.99d (TeX Live 2022/dev/Debian) +Capacity: max_strings=200000, hash_size=200000, hash_prime=170003 +The top-level auxiliary file: document.aux +The style file: plain.bst +Database file #1: refs.bib +You've used 3 entries, + 2118 wiz_defined-function locations, + 521 strings with 4580 characters, +and the built_in function-call counts, 1233 in all, are: += -- 127 +> -- 46 +< -- 1 ++ -- 17 +- -- 14 +* -- 90 +:= -- 198 +add.period$ -- 10 +call.type$ -- 3 +change.case$ -- 15 +chr.to.int$ -- 0 +cite$ -- 3 +duplicate$ -- 45 +empty$ -- 102 +format.name$ -- 14 +if$ -- 263 +int.to.chr$ -- 0 +int.to.str$ -- 3 +missing$ -- 3 +newline$ -- 18 +num.names$ -- 8 +pop$ -- 13 +preamble$ -- 1 +purify$ -- 12 +quote$ -- 0 +skip$ -- 35 +stack$ -- 0 +substring$ -- 112 +swap$ -- 13 +text.length$ -- 1 +text.prefix$ -- 0 +top$ -- 0 +type$ -- 12 +warning$ -- 0 +while$ -- 14 +width$ -- 4 +write$ -- 36 diff --git a/document/document.tex b/document/document.tex new file mode 100644 index 0000000..f030a5b --- /dev/null +++ b/document/document.tex @@ -0,0 +1,397 @@ +\documentclass{article} + +\usepackage{natbib} + +\input{common} + +\title{AFT and HMKNF} +\author{} +\date{May 25th 2023} + +\begin{document} +\maketitle + + +\section{An Approximator Hybrid MKNF knowledge bases} + +The lattice $\langle \L^2, \preceq_p \rangle$ + +\begin{align*} + \Gamma(T, P) &\define \{ \head(r) ~|~ r \in \P,~ T \subseteq \bodyp(r),~ \bodyn(r) \intersect P = \emptyset \}\\ + extract(T) &\define \{ a \in \L ~|~ \OBO{T} \models \neg a \} \\ + \Phi(T, P) &\define \Bigl( \Gamma(T, P), \Gamma(P, T) \setminus extract(T) \Bigr) +\end{align*} + +\begin{align*} + S(\Phi)(T, P) \define \Bigl( \lfp~\Gamma(\cdot, P),~ \lfp\,\Bigl( \Gamma(\cdot, T) \setminus extract(T) \Bigr) \Bigr) +\end{align*} + +\appendix + +\section{Lattice Theory} + +\begin{definition} + A {\em partial order} $\preceq$ is a relation over a set $S$ such that for every triple of elements $x, y, z \in S$ the following hold + \begin{itemize} + \item (reflexivity) $x \preceq x$ + \item (antisymmetry) $(x \preceq y \land y \preceq x) \implies x = y$ + \item (transitivity) $(x \preceq y \land y \preceq z) \implies (x \preceq z)$ + \end{itemize} +\end{definition} + + +\begin{definition} + Given a partial order $\preceq$ over a set $S$ and a subset $X \subseteq S$, a {\em lower bound} of $X$ (resp.\ an {\em upper bound} of $X$) is an element $x \in S$ (Note that it may be the case that $x \not\in X$) such that + \begin{itemize} + \item $\forall y \in X, \boxed{x} \preceq y$ + \item (resp. $\forall y \in X, \boxed{y} \preceq x$) + \end{itemize} + The {\em greatest lower bound} of a set $X \subseteq S$ (denoted as $\textbf{glb}(X)$) is a unique upperbound of the set of all lowerbounds of $X$. + The {\em least upper bound} of a set $X \subseteq S$ (denoted as $\textbf{lub}(X)$) is a unique lowerbound of the set of all upperbounds of $X$. + In general, $\textbf{lub}(X)$ and $\textbf{glb}(X)$ may not exist. +\end{definition} + +\begin{definition} + A (complete) lattice $\langle \mathcal{L}, \preceq \rangle$ is a set of elements $\mathcal{L}$ and a partial order $\preceq$ over $\mathcal{L}$ such that for any set $S \subseteq \mathcal{L}$ + \begin{itemize} + \item $\textbf{lub}(X)$ and $\textbf{glb}(X)$ exist and are unique. + \end{itemize} +\end{definition} + + +\section{Partial Stable Model Semantics} + +\begin{definition} + A (ground and normal) {\em answer set program} $\P$ is a set of rules where each rule $r$ is of the form + \begin{align*} + h \leftarrow a_0,~ a_1,~ \dots,~ a_n,~ \Not b_0,~\Not b_1,~\dots,~\Not b_k + \end{align*} + where we define the following shorthand for a rule $r \in \P$ + \begin{align*} + \head(r) &= h\\ + \bodyp(r) &= \{ a_0,~ a_1,~ \dots,~ a_n \}\\ + \bodyn(r) &= \{ b_0,~ b_1,~ \dots,~ b_k \} + \end{align*} +\end{definition} + +\begin{definition} + A two-valued interpretation $I$ of a program $\P$ is a set of atoms that appear in $\P$. +\end{definition} + +\begin{definition} + An interpretation $I$ is a \boxedt{model} of a program $\P$ if for each rule $r \in \P$ + \begin{itemize} + \item If $\bodyp(r) \subseteq I$ and $\bodyn(r) \intersect I = \emptyset$ then $\head(r) \in I$. + \end{itemize} +\end{definition} + +\begin{definition} + An interpretation $I$ is a \boxedt{stable model} of a program $\P$ if $I$ is a model of $\P$ \textbf{and} + for every interpretation $I' \subseteq I$ there exists a rule $r \in \P$ such that + \begin{itemize} + \item $\bodyp(r) \subseteq I'$, $\bodyn(r) \intersect I \not= \emptyset$ (Note that this is $I$ and not $I'$) and $\head(r) \not\in I'$ + \end{itemize} +\end{definition} + +\begin{definition} + A three-valued interpretation $(T, P)$ of a program $\P$ is a pair of sets of atoms such that $T \subseteq P$. + The \boxedt{truth-ordering} respects $\ff < \uu < \tt$ and is defined for two three-valued interpretations $(T, P)$ and $(X, Y)$ as follows. + \begin{align*} + (T, P) \preceq_t (X, Y) \textrm{ iff } T \subseteq X \land P \subseteq Y + \end{align*} + The \boxedt{precision-ordering} respects the partial order $\uu < \tt$, $\uu < \ff$ and is defined for two three-valued interpretations $(T, P)$ and $(X, Y)$ as follows. + \begin{align*} + (T, P) \preceq_p (X, Y) \textrm{ iff } T \subseteq X \land \boxed{Y \subseteq P} + \end{align*} +\end{definition} + +\begin{definition} + A three-valued interpretation $(T, P)$ is a {\em model} of a program $\P$ if for each rule $r \in \P$ + \begin{itemize} + \item $\body(r) \subseteq P \land \bodyn(r) \intersect T = \emptyset$ implies $\head(r) \in P$, and + \item $\body(r) \subseteq T \land \bodyn(r) \intersect P = \emptyset$ implies $\head(r) \in T$. + \end{itemize} +\end{definition} + +\begin{definition} + A three-valued interpretation $(T, P)$ is a {\em stable model} of a program $\P$ if it is a model of $\P$ and if for every three-valued interpretation $(X, Y)$ such that $(X, Y) \preceq_t (T, P)$ there exists a rule $r \in \P$ such that either + \begin{itemize} + \item $\bodyp(r) \subseteq Y \land \bodyn(r) \intersect T = \emptyset$ and $\head(r) \not\in Y$ \textbf{OR} + \item $\bodyp(r) \subseteq X \land \bodyn(r) \intersect P = \emptyset$ and $\head(r) \not\in X$ + \end{itemize} +\end{definition} + + +\subsection{Fixpoint Operators} + +\begin{definition} + Given a complete lattice $\langle \mathcal{L}, \preceq \rangle$, a fixpoint operator over the lattice is a function $\Phi: \mathcal{L} \rightarrow \mathcal{L}$ that is {\em $\preceq$-monotone} + \begin{itemize} + \item $\Phi$ is $\preceq$-monotone if for all $x, y \in \mathcal{L}$ + \begin{align*} + x \preceq y \implies \Phi(x) \preceq \Phi(y) + \end{align*} + (Note: this does not mean the function is inflationary, i.e., $x \preceq \Phi(x)$ may not hold) + \end{itemize} + A {\em fixpoint} is an element $x \in \mathcal{L}$ s.t. $\Phi(x) = x$. +\end{definition} + +\begin{theorem}[Knaster-Tarski] + The set of all fixpoints of a fixpoint operator $\Phi$ on a complete lattice is itself a complete lattice. The least element of this new lattice exists and is called the least fixpoint (denoted as $\lfp~{\Phi}$) +\end{theorem} + +Some intuitions about lattices +\begin{itemize} + \item The entire lattice has a biggest element $\lub{}(\mathcal{L}) = \top$ and a smallest element $\glb{}(\mathcal{L}) = \bot$ + \item When a lattice has a finite height (or finite domain). The least fixed point of a fixpoint operator can be computed by iteratively applying the fixpoint operator to $\bot$ + \item An operator may return an element that is not comparable to the input, however, after a comparable element is returned (either greater or less than) that comparability and direction are maintained for all subsequent iterations. + \item Further, because $\bot$ is less than all elements in the lattice, it is always the case that $\bot \preceq \Phi(\bot)$ +\end{itemize} + + +\section{Approximation Fixpoint Theory} + +We can think of a three-valued interpretation $(T, P)$ as an approximation on the set of true atoms. +$T$ is a lower bound and $P$ is the upper bound. + +\begin{definition} + An {\em approximator} is a fixpoint operator on the complete lattice $\langle \wp(\mathcal{L})^2, \preceq_p \rangle$ (called a bilattice) +\end{definition} +Given a function $f(T, P): S^2 \rightarrow S^2$, we define two separate functions +\begin{align*} + f(\cdot, P)_1:~ &S \rightarrow S\\ + f(T, \cdot)_2:~ &S \rightarrow S +\end{align*} +such that +\begin{align*} + f(T, P) = \Big(&(f(\cdot, P)_1)(T), \\&(f(T, \cdot)_2)(P)\Big) +\end{align*} + +\begin{definition} + Given an approximator $\Phi(T, P)$ the stable revision operator is defined as follows + \begin{align*} + S(T, P) = (\lfp{(\Phi(\cdot, P)_1)},~ \lfp{(\Phi(T, \cdot)_2)}) + \end{align*} + Note: the $\lfp$ is applied to a unary operator, thus it's the least fixpoint of the lattice $\langle \wp(\mathcal{L}), \subseteq \rangle$ whose least element is $\emptyset$. +\end{definition} + + +\section{Hybrid MKNF Knowledge Bases}\label{section-prelim-hmknf} + +Motik and Rosati \cite{motikreconciling2010} extend MKNF (Minimal Knowledge and Negation as Failure \cite{lifschitznonmonotonic1991}) to form hybrid MKNF, a nonmonotonic logic that supports classical reasoning with ontologies. +We use Knorr et al.'s \cite{knorrlocal2011} \mbox{3-valued} semantics for hybrid MKNF; +Under which there are three truth values: $\ff$ (false), $\uu$ (undefined), and $\tt$ (true) that use the +ordering $\ff < \uu < \tt$. +The $min$ and $max$ functions respect this ordering when applied to sets. + +MKNF relies on the standard name assumption under which +every first-order interpretation in an +MKNF interpretation is required to be a Herbrand interpretation with a +countably infinite amount of additional constants. +We use $\Delta$ to denote the set of all these constants. +We use $\phi[x \rightarrow \alpha]$ to denote the formula obtained by replacing all free +occurrences of variable x in $\phi$ with the term $\alpha$. + +A (\mbox{3-valued}) \textit{MKNF structure} is a triple $(I, \M, \N)$ where $I$ is +a (two-valued first-order) interpretation and $\M = \langle M, M_1 \rangle$ and +$\N = \langle N, N_1 \rangle$ are pairs of sets of first-order interpretations +such that $M \supseteq M_1$ and $N \supseteq N_1$. +Using $\phi$ and $\sigma$ to denote MKNF formulas, the evaluation of an MKNF +structure is defined as follows: +\begin{align*} + &(I, \M, \N)({p(t_1, \dots ,~t_n)}) \define + \left\{\begin{array}{ll} + \tt & \textrm{iff } p(t_1, \dots,~t_n) \textrm{ is \boxed{\textrm{true}} in } I + \\ + \ff & \textrm{iff } p(t_1, \dots,~t_n) \textrm{ is \boxed{\textrm{false}} in } I + \\ + \end{array}\right. + \\ + &(I, \M, \N)({\neg \phi}) \define + \left\{\begin{array}{ll} + \tt & \textrm{iff } (I, \M, \N)({\phi}) = \ff \\ + \uu & \textrm{iff } (I, \M, \N)({\phi}) = \uu \\ + \ff & \textrm{iff } (I, \M, \N)({\phi}) = \tt \\ + \end{array}\right. + \\ + &(I, \M, \N)({\exists x, \phi}) \define max\{(I, \M, + \N)({\phi[\alpha \rightarrow x]}) ~|~\alpha \in \Delta\} + \\ + &(I, \M, \N)({\forall x, \phi}) \define min\{(I, \M, + \N)({\phi[\alpha \rightarrow x]}) ~|~\alpha \in \Delta\} + \\ + &(I, \M, \N)({\phi \land \sigma}) \define min((I, \M, \N)({\phi}), (I, + \M, \N)({\sigma})) + \\ + &(I, \M, \N)({\phi \lor \sigma}) \define max((I, \M, \N)({\phi}), (I, + \M, \N)({\sigma})) + \\ + &(I, \M, \N)({\phi \subset \sigma}) \define \left\{ \begin{array}{ll} + \tt & \textit{iff }\vspace{0.3em} (I, \M, + \N)({\phi}) \geq (I, \M, \N)({\sigma}) \\ + \ff & \textrm{otherwise} + \end{array}\right.\\ + &(I, \M, \N)({\bfK \phi}) \define + \left\{\begin{array}{ll} + \tt & \textrm{iff } (J, \MM, \N)({\phi}) = \tt \textrm{ \boxedt{for all} + } J + \in M + \\ + \ff & \textrm{iff } (J, \MM, \N)({\phi}) = \ff \textrm{ \boxedt{for some} } J + \in M_1 + \\ + \uu & \textrm{otherwise} + \end{array}\right. + \\ + &(I, \M, \N)({\Not \phi}) \define + \left\{\begin{array}{ll} + \tt & \textrm{iff } (J, \M, \NN)({\phi}) = \ff \textrm{ \boxedt{for some} } J + \in N_1 + \\ + \ff & \textrm{iff } (J, \M, \NN)({\phi}) = \tt \textrm{ \boxedt{for all} } J + \in N + \\ + \uu & \textrm{otherwise} + \end{array}\right. +\end{align*} + +While this logic captures many nonmonotonic semantics, we restrict our focus to hybrid MKNF Knowledge bases, +a syntactic restriction that captures combining answer set programs with ontologies. +An (MKNF) program $\P$ is a set of (MKNF) rules. A rule $r$ is written as +follows: +\begin{align*}\label{MKNFRules} + \bfK h \leftarrow \bfK p_0,\dots,~\bfK p_j,~ \Not n_0,\dots,~\Not n_k. +\end{align*} +In the above, the atoms $h, p_0, n_0, \dots, p_j, $ and $n_k $ are function-free first-order +atoms +of the form $p(t_0, \dots,~t_n )$ where $p$ is a predicate and $t_0, + \dots,~t_n$ are either constants or variables. +We call an MKNF formula $\phi$ \textit{ground} if it does not contain variables. +The corresponding MKNF formula $\pi(r)$ for a rule $r$ is as follows: +\begin{align*} + \pi(r) \define \forall \vec{x},~ \bfK h \subset \bfK p_0 \land \dots \land + \bfK p_j \land \Not n_0 \land \dots \land \Not n_k +\end{align*} +where $\vec{x}$ is a vector of all variables appearing in the rule. +We will use the following abbreviations: +\begin{align*} + &\pi(\P) \define \bigwedge\limits_{r \in \P} \pi(r)\\ + &\head(r) = \bfK h \\ + &\bodyp(r) = \{ \bfK p_0, \dots,~ \bfK p_j \} \\ + &\bodyn(r) = \{ \Not n_0, \dots,~ \Not n_k \} \\ + &\bfK(\bodyn(r)) = \{ \bfK a ~|~ \Not a \in \bodyn(r) \} +\end{align*} +An \textit{ontology} $\OO$ is a decidable description logic (DL) knowledge base translatable to first-order logic, we denote its translation to first-order logic with $\pi(\OO)$. +We also assume that the ontology's entailment relation can be checked in polynomial time. + +A {\em normal hybrid MKNF knowledge base} (or knowledge base for short) $\KB + = (\OO, \P)$ contains a program and an ontology. +The semantics of a knowledge base corresponds to the MKNF formula $\pi(\KB) = \pi(\P) \land \bfK \pi(\O)$. +We assume, without loss of generality \cite{knorrlocal2011}, that any given hybrid MKNF knowledge $\KB = (\OO, \P)$ base is ground, that is, $\P$, does not contain any variables\footnote{Not every knowledge base can be grounded. The prevalent class of groundable knowledge bases is the knowledge bases that are DL-safe~\cite{motikreconciling2010}.} +This ensures that $\KB$ is decidable. + +A {\em (\mbox{3-valued}) MKNF interpretation} $(M, N)$ is a pair of sets of +first-order interpretations where $\emptyset \subset N \subseteq M$. +We say an MKNF interpretation $(M, N)$ \textit{satisfies} a knowledge base $\KB + = (\OO, \P)$ if for each $I \in M$, +$(I, \MN, \MN) (\pi (\KB)) = \tt$. + +\begin{definition} \label{model} + A (\mbox{3-valued}) MKNF interpretation $(M, N)$ is a + \textit{(\mbox{3-valued}) MKNF model} of a normal hybrid MKNF knowledge base + $\KB$ + if $(M, N)$ satisfies $\pi(\KB)$ and for every \mbox{3-valued} MKNF + interpretation pair $(M', N')$ where $M \subseteq M'$, $N \subseteq N'$, + $(M, N) \not= (M', N')$, and we have some $I \in M'$ s.t. $(I, \langle M', N' + \rangle, \MN)(\pi(\KB)) \not= \tt$. +\end{definition} + +It is often convenient to only deal with atoms that appear inside $\P$. +We use $\KAK$ to denote the set of \Katoms{} that appear as either $\bfK a$ or $\Not a$ in the program and we use $\OBO{S}$ to the objective knowledge w.r.t.\ to a set of \Katoms{} $S$. +\begin{align*} + \KAK &\define \{ \bfK a ~|~ r \in \P,~ \bfK a \in \Big(\{ \head(r) \} \union + \bodyp(r) \union \bfK(\bodyn(r)) \Big) \} \\ + \OBO{S} &\define \big\{ \pi(\OO) \big\} \union \big\{ a ~|~ \bfK a \in S + \} +\end{align*} +A \textit{$\bfK$-interpretation} $(T, P) \in \wp(\KAK)^2$ is a pair of sets of \Katoms{}\footnote{We use $\wp(S)$ to denote the powerset of $S$, i.e., $\wp(S) = \{ X ~|~ X \subseteq S \}$}. +We say that $(T, P)$ is consistent if $T \subseteq P$. +An MKNF interpretation pair $(M, N)$ uniquely {\em induces} a consistent \bfK-interpretation $(T, P)$ where for +each $\bfK a \in \KAK$: +\begin{align*} + \bfK a \in \boxed{(T \intersect P)} \textrm{ if } \forall I \in M, \mmeval{\bfK a} &= \boxed{\tt}\\ + \bfK a \not\in \boxed{\hspace{0.5cm} P \hspace{0.5cm}} \textrm{ if } \forall I \in M, \mmeval{\bfK a} &= \boxed{\ff}\\ + \bfK a \in \boxed{(P \setminus T)} \textrm{ if } \forall I \in M, \mmeval{\bfK a} &= \boxed{\uu} +\end{align*} +We can acquire the set of false \Katoms{} by taking the complement of $P$, e.g., $F = \KAK \setminus P$ and $P = \KAK \setminus F$. +When we use the letters $T$, $P$, and $F$, we always mean sets of true, possibly true, and false \Katoms{} respectively. + + +We say that a \bfK-interpretation $(T, P)$ \textit{extends} to an MKNF interpretation $(M, N)$ if $(T, P)$ is consistent, $\OBO{P}$ is consistent, and +\begin{align*} + (M, N) = (\{ I ~|~ \OBO{T} \models I \}, \{ I ~|~ \OBO{P} \models I \}) +\end{align*} +This operation extends $(T, P)$ to the $\subseteq$-maximal MKNF interpretation that induces $(T, P)$. + + +We comment on how the relation \textit{induces} and \textit{extends} are related. +\begin{remark} + Let $(M, N)$ be an MKNF {\bf model} of an MKNF knowledge base $\KB$. + A \bfK-interpretation $(T, P)$ that extends to $(M, N)$ exists, is unique, and is the \bfK-interpretation induced by $(M, N)$. +\end{remark} +We say that an MKNF interpretation $(M, N)$ \textit{weakly induces} a {\bfK-interpretation} $(T, P)$ if $(M, N)$ induces a {\bfK-interpretation} $(T^*, P^*)$ where $T \subseteq T^*$ and $P^* \subseteq P$. +Similarly, a {\bfK-interpretation} \textit{weakly extends} to an MKNF interpretation $(M, N)$ if there exists an interpretation $(T^*, P^*)$ that extends to $(M, N)$ such that $T \subseteq T^*$, $P^* \subseteq P$. +Intuitively, we are leveraging the knowledge ordering $\uu < \tt$ and $\uu < \ff$. A \bfK-interpretation is weakly induced by an MKNF interpretation if that MKNF interpretation induces a \bfK-interpretation that ``knows more'' than the original \bfK-interpretation. + +There are MKNF interpretations for which no \bfK-interpretation extends to, however, these are of little interest; either $\OBO{P}$ is inconsistent or $(M, N)$ is not maximal w.r.t. atoms that do not appear in $\KAK$. Similarly, there exist \bfK-interpretations that extend to MKNF interpretations that do not induce them. If this is the case, then the \bfK-interpretation is missing some logical consequences of the ontology and this should be corrected. +We define the class of \bfK-interpretations that excludes the undesirable \bfK-interpretations and MKNF interpretations from focus. +\begin{definition}\label{saturated} + A \bfK-interpretation $(T, P)$ of an MKNF knowledge base $\KB$ is {\em saturated} if it can be extended to an MKNF interpretation $(M, N)$ that induces $(T, P)$. + Equivalently, a \bfK-interpretation is saturated iff $(T, P)$ and $\OBO{P}$ are consistent, + $ \OBO{P} \not\models a~\textrm{for each } \bfK a \in (\KAK \setminus P)$ and $\OBO{T} \not\models a~\textrm{for each } \bfK a \in (\KAK \setminus T)$. +\end{definition} + +\subsection{An Example Knowledge Base} +Hybrid MKNF is equivalent to answer set semantics when the ontology is empty. +The definition of an MKNF program given above is precisely the formulation of stable model semantics in the logic of MKNF~\cite{lifschitznonmonotonic1991}. +We give an example of a knowledge base to demonstrate the combined reasoning of an answer set program with an ontology. +\begin{example} +Let $\KB = (\OO, \P)$ be the following knowledge base +\begin{align*} + \pi(\OO) &= \{ a \lor \neg b \} \\ + (\textrm{The definition of } &\P \textrm{ follows})\\ + \bfK a &\leftarrow \Not b\\ + \bfK b &\leftarrow \Not a +\end{align*} +This knowledge base has two MKNF models +\begin{align*} + &\Big(\Big\{\{ a, b \}, \{ a, \neg b\}, \{ \neg a, \neg b \}\Big\}, \Big\{\{ a, b \} \Big\}\Big) \\ + &\hspace{1cm}\textrm{ which induces the \bfK-interpretation } (\emptyset, \{ \bfK a, \bfK b \})\\ + &(M, M) \textrm{ where } M = \Big\{\{ a, \neg b\}, \{ a, b \} \Big\}\\ + &\hspace{1cm}\textrm{ which induces the \bfK-interpretation } (\{ \bfK a \}, \{ \bfK a \}) +\end{align*} +Above we have the answer set program $\P$ that, without $\OO$, admits three partial stable models. The ontology $\OO$ encodes an exclusive choice between the atoms $a$ and $b$. The program allows for both $a$ and $b$ to be undefined. +The use of the ontology here is effectively a filter that removes all interpretations where $a$ is false but $b$ is true. + +The mixing of negation as failure and classical negation is not always straightforward. For example +\begin{align*} + \pi(\OO) &= \{ a \lor b \} \\ + \P &= \emptyset +\end{align*} +The above admits just one MKNF model +\begin{align*} + &\big(M, M \big) \textrm{ where } M = \Big\{ \{ a, \neg b \}, \{ \neg a, b \}, \{ a, b \} \Big\}\\ + &\hspace{1cm}\textrm{ which induces the \bfK-interpretation } (\emptyset, \emptyset) +\end{align*} +From the perspective of $\P$, which is only concerned with \bfK-interpretations, all atoms are false. +However, the interpretation $\{ \neg a, \neg b \}$ is absent from the model which ensures that $\O$ is still satisfied. +Recall that $\pi(\KB) = \bfK (a \lor b)$. + +\end{example} + + +\bibliographystyle{plain} +\bibliography{refs} + + +\end{document} \ No newline at end of file diff --git a/document/refs.bib b/document/refs.bib new file mode 100644 index 0000000..f064386 --- /dev/null +++ b/document/refs.bib @@ -0,0 +1,453 @@ + +@book{romanlattices2008, + location = {New York, {NY}}, + title = {Lattices and Ordered Sets}, + isbn = {978-0-387-78900-2 978-0-387-78901-9}, + url = {http://link.springer.com/10.1007/978-0-387-78901-9}, + publisher = {Springer New York}, + author = {Roman, Steven}, + urldate = {2021-07-28}, + year = {2008}, + langid = {english}, + doi = {10.1007/978-0-387-78901-9}, + file = {2008 - Lattices and Ordered Sets.pdf:/home/capybara/Zotero/storage/5QU8WTUR/2008 - Lattices and Ordered Sets.pdf:application/pdf}, +} + +@InProceedings{RRaft, +author="Bi, Yi +and You, Jia-Huai +and Feng, Zhiyong", +editor="Kontchakov, Roman +and Mugnier, Marie-Laure", +title="A Generalization of Approximation Fixpoint Theory and Application", +booktitle="Web Reasoning and Rule Systems", +year="2014", +publisher="Springer International Publishing", +address="Cham", +pages="45--59" +} + + +@article{gelfondstable2000, +title = {The Stable Model Semantics For Logic Programming}, +volume = {2}, +abstract = {We propose a new declarative semantics for logic programs with negation. Its formulation is quite simple; at the same time, it is more general than the iterated xed point semantics for stratied programs, and is applicable to some useful programs that are not stratied.}, +journal = {Logic Programming}, +shortjournal = {Logic Programming}, +author = {Gelfond, Michael and Lifschitz, Vladimir}, +date = {2000-12-14}, +year = "2000", +file = {Full Text PDF:/home/gopher/Zotero/storage/LSRXUIBD/The_Stable_Model_Semantics_For_Logic_Programming.pdf:application/pdf} +} + + + + +@inproceedings{aftjust, + author = {Simon Marynissen and + Bart Bogaerts and + Marc Denecker}, + editor = {Zhi{-}Hua Zhou}, + title = {On the Relation Between Approximation Fixpoint Theory and Justification + Theory}, + booktitle = {Proceedings of the Thirtieth International Joint Conference on Artificial + Intelligence, {IJCAI} 2021, Virtual Event / Montreal, Canada, 19-27 + August 2021}, + pages = {1973--1980}, + publisher = {ijcai.org}, + year = {2021}, + url = {https://doi.org/10.24963/ijcai.2021/272}, + doi = {10.24963/ijcai.2021/272}, + timestamp = {Sat, 09 Apr 2022 12:47:19 +0200}, + biburl = {https://dblp.org/rec/conf/ijcai/Marynissen0D21.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + + + +@article{liuyou2021, +author = {Fangfang Liu and + Jia{-}Huai You}, +title = {Alternating Fixpoint Operator for Hybrid {MKNF} Knowledge Bases as + an Approximator of {AFT}}, +journal = {Theory Pract. Log. Program.}, +volume = {22}, +number = {2}, +pages = {305--334}, +year = {2022}, +doi = {10.1017/S1471068421000168}, +timestamp = {Wed, 27 Apr 2022 20:10:27 +0200}, +biburl = {https://dblp.org/rec/journals/tplp/LiuY22.bib}, +bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{liuyou2019, + author = {Fangfang Liu and + Jia{-}Huai You}, + editor = {Paul Fodor and + Marco Montali and + Diego Calvanese and + Dumitru Roman}, + title = {Alternating Fixpoint Operator for Hybrid {MKNF} Knowledge Bases as + an Approximator of {AFT}}, + booktitle = {Rules and Reasoning - Third International Joint Conference, RuleML+RR + 2019, Bolzano, Italy, September 16-19, 2019, Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = {11784}, + pages = {113--127}, + publisher = {Springer}, + year = {2019}, + url = {https://doi.org/10.1007/978-3-030-31095-0\_8}, + doi = {10.1007/978-3-030-31095-0\_8}, + timestamp = {Tue, 17 Sep 2019 08:40:59 +0200}, + biburl = {https://dblp.org/rec/conf/ruleml/LiuY19.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + + +@article{aftagg, + author = {Linde Vanbesien and + Maurice Bruynooghe and + Marc Denecker}, + title = {Analyzing Semantics of Aggregate Answer Set Programming Using Approximation + Fixpoint Theory}, + journal = {Theory Pract. Log. Program.}, + volume = {22}, + number = {4}, + pages = {523--537}, + year = {2022}, + url = {https://doi.org/10.1017/S1471068422000126}, + doi = {10.1017/S1471068422000126}, + timestamp = {Sat, 10 Sep 2022 20:58:45 +0200}, + biburl = {https://dblp.org/rec/journals/tplp/VanbesienBD22.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + + + +@article{DeneckerMT04, +author = {Marc Denecker and + Victor W. Marek and + Miroslaw Truszczynski}, +title = {Ultimate approximation and its application in nonmonotonic knowledge + representation systems}, +journal = {Inf. Comput.}, +volume = {192}, +number = {1}, +pages = {84--121}, +year = {2004}, +doi = {10.1016/j.ic.2004.02.004}, +timestamp = {Fri, 12 Feb 2021 22:16:22 +0100}, +biburl = {https://dblp.org/rec/journals/iandc/DeneckerMT04.bib}, +bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@incollection{denecker2000approximations, +title={Approximations, stable operators, well-founded fixpoints and applications in nonmonotonic reasoning}, +author={Denecker, Marc and Marek, Victor and Truszczy{\'n}ski, Miros{\l}aw}, +booktitle={Logic-Based Artificial Intelligence}, +pages={127--144}, +year={2000}, +doi={10.1007/978-1-4615-1567-8_6}, +publisher = {Springer}, +} + +@article{fittingfixpointsurvey, + author = {Melvin Fitting}, + title = {Fixpoint semantics for logic programming a survey}, + journal = {Theor. Comput. Sci.}, + volume = {278}, + number = {1-2}, + pages = {25--51}, + year = {2002}, + url = {https://doi.org/10.1016/S0304-3975(00)00330-3}, + doi = {10.1016/S0304-3975(00)00330-3}, + timestamp = {Wed, 17 Feb 2021 21:58:01 +0100}, + biburl = {https://dblp.org/rec/journals/tcs/Fitting02.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{Ji17, +author = {Jianmin Ji and + Fangfang Liu and + Jia{-}Huai You}, +title = {Well-founded operators for normal hybrid {MKNF} knowledge bases}, +journal = {Theory Pract. Log. Program.}, +volume = {17}, +number = {5-6}, +pages = {889--905}, +year = {2017}, +doi = {10.1017/S1471068417000291}, +timestamp = {Mon, 26 Oct 2020 08:22:48 +0100}, +biburl = {https://dblp.org/rec/journals/tplp/JiLY17.bib}, +bibsource = {dblp computer science bibliography, https://dblp.org} +} + + +@article{Fitting02, +author = {Melvin Fitting}, +title = {Fixpoint semantics for logic programming a survey}, +journal = {Theor. Comput. Sci.}, +volume = {278}, +number = {1-2}, +pages = {25--51}, +year = {2002}, +doi = {10.1016/S0304-3975(00)00330-3}, +timestamp = {Wed, 17 Feb 2021 21:58:01 +0100}, +biburl = {https://dblp.org/rec/journals/tcs/Fitting02.bib}, +bibsource = {dblp computer science bibliography, https://dblp.org} +}} + + +@article{knorrlocal2011, +author = {Matthias Knorr and + Jos{\'{e}} J{\'{u}}lio Alferes and + Pascal Hitzler}, +title = {Local closed world reasoning with description logics under the well-founded + semantics}, +journal = {Artif. Intell.}, +volume = {175}, +number = {9-10}, +pages = {1528--1554}, +year = {2011}, +doi = {10.1016/j.artint.2011.01.007}, +timestamp = {Wed, 23 Feb 2022 14:32:41 +0100}, +biburl = {https://dblp.org/rec/journals/ai/KnorrAH11.bib}, +bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{przymusinskistable1991, +author = {Teodor C. Przymusinski}, +title = {Stable Semantics for Disjunctive Programs}, +journal = {New Gener. Comput.}, +volume = {9}, +number = {3/4}, +pages = {401--424}, +year = {1991}, +doi = {10.1007/BF03037171}, +timestamp = {Thu, 14 May 2020 22:23:50 +0200}, +biburl = {https://dblp.org/rec/journals/ngc/Przymusinski91.bib}, +bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{lifschitznonmonotonic1991, +author = {Vladimir Lifschitz}, +editor = {John Mylopoulos and + Raymond Reiter}, +title = {Nonmonotonic Databases and Epistemic Queries}, +booktitle = {Proceedings of the 12th International Joint Conference on Artificial + Intelligence. Sydney, Australia, August 24-30, 1991}, +pages = {381--386}, +publisher = {Morgan Kaufmann}, +year = {1991}, +url = {http://ijcai.org/Proceedings/91-1/Papers/059.pdf}, +timestamp = {Tue, 20 Aug 2019 16:18:13 +0200}, +biburl = {https://dblp.org/rec/conf/ijcai/Lifschitz91.bib}, +bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{motikreconciling2010, +author = {Boris Motik and + Riccardo Rosati}, +title = {Reconciling description logics and rules}, +journal = {J. {ACM}}, +volume = {57}, +number = {5}, +pages = {30:1--30:62}, +year = {2010}, +doi = {10.1145/1754399.1754403}, +timestamp = {Mon, 16 Sep 2019 14:49:47 +0200}, +biburl = {https://dblp.org/rec/journals/jacm/MotikR10.bib}, +bibsource = {dblp computer science bibliography, https://dblp.org} +} + + + +@article{liuthreevalued2017, +author = {Fangfang Liu and + Jia{-}Huai You}, +title = {Three-valued semantics for hybrid {MKNF} knowledge bases revisited}, +journal = {Artif. Intell.}, +volume = {252}, +pages = {123--138}, +year = {2017}, +doi = {10.1016/j.artint.2017.08.003}, +timestamp = {Thu, 28 Dec 2017 16:12:02 +0100}, +biburl = {https://dblp.org/rec/journals/ai/LiuY17.bib}, +bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{revisited, + author = {Fangfang Liu and + Jia{-}Huai You}, + title = {Three-valued semantics for hybrid {MKNF} knowledge bases revisited}, + journal = {Artif. Intell.}, + volume = {252}, + pages = {123--138}, + year = {2017}, + url = {https://doi.org/10.1016/j.artint.2017.08.003}, + doi = {10.1016/j.artint.2017.08.003}, + timestamp = {Thu, 28 Dec 2017 16:12:02 +0100}, + biburl = {https://dblp.org/rec/journals/ai/LiuY17.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + + +@article{tarskilatticetheoretical1955, +author = {Alfred Tarski}, +title = {{A lattice-theoretical fixpoint theorem and its applications.}}, +volume = {5}, +journal = {Pacific Journal of Mathematics}, +number = {2}, +publisher = {Pacific Journal of Mathematics, A Non-profit Corporation}, +pages = {285 -- 309}, +doi = {10.2140/pjm.1955.5.285}, +year = {1955} +} + +@article{gebserconflictdriven2012, +author = {Martin Gebser and + Benjamin Kaufmann and + Torsten Schaub}, +title = {Conflict-driven answer set solving: From theory to practice}, +journal = {Artif. Intell.}, +volume = {187}, +pages = {52--89}, +year = {2012}, +doi = {10.1016/j.artint.2012.04.001}, +timestamp = {Fri, 09 Apr 2021 18:34:15 +0200}, +biburl = {https://dblp.org/rec/journals/ai/GebserKS12.bib}, +bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{gebseradvanced2013, +author = {Martin Gebser and + Benjamin Kaufmann and + Torsten Schaub}, +editor = {Francesca Rossi}, +title = {Advanced Conflict-Driven Disjunctive Answer Set Solving}, +booktitle = {{IJCAI} 2013, Proceedings of the 23rd International Joint Conference + on Artificial Intelligence, Beijing, China, August 3-9, 2013}, +pages = {912--918}, +publisher = {{IJCAI/AAAI}}, +year = {2013}, +url = {http://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/view/6835}, +timestamp = {Tue, 08 Mar 2022 17:41:53 +0100}, +biburl = {https://dblp.org/rec/conf/ijcai/GebserKS13.bib}, +bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{killenfixpoint2021, +author = {Spencer Killen and + Jia{-}Huai You}, +title = {Fixpoint Characterizations of Disjunctive Hybrid {MKNF} Knowledge + Bases}, +booktitle = {Proceedings of the International Conference on Logic Programming 2021 + Workshops co-located with the 37th International Conference on Logic + Programming {(ICLP} 2021), Porto, Portugal (virtual), September 20th-21st, + 2021}, +series = {{CEUR} Workshop Proceedings}, +volume = {2970}, +publisher = {CEUR-WS.org}, +year = {2021}, +url = {http://ceur-ws.org/Vol-2970/aspocppaper3.pdf}, +timestamp = {Thu, 28 Oct 2021 14:11:18 +0200}, +biburl = {https://dblp.org/rec/conf/iclp/KillenY21.bib}, +bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{killen2022, + author = {Spencer Killen and + Jia{-}Huai You}, + editor = {Yuliya Lierler and + Jos{\'{e}} F. Morales and + Carmine Dodaro and + Ver{\'{o}}nica Dahl and + Martin Gebser and + Tuncay Tekle}, + title = {A Fixpoint Characterization of Three-Valued Disjunctive Hybrid {MKNF} + Knowledge Bases}, + booktitle = {Proceedings 38th International Conference on Logic Programming, {ICLP} + 2022 Technical Communications / Doctoral Consortium, Haifa, Israel, + 31st July 2022 - 6th August 2022}, + series = {{EPTCS}}, + volume = {364}, + pages = {51--64}, + year = {2022}, + url = {https://doi.org/10.4204/EPTCS.364.6}, + doi = {10.4204/EPTCS.364.6}, + timestamp = {Sat, 15 Oct 2022 11:57:01 +0200}, + biburl = {https://dblp.org/rec/journals/corr/abs-2208-03087.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{killenunfounded, +author = {Spencer Killen and + Jia{-}Huai You}, +editor = {Meghyn Bienvenu and + Gerhard Lakemeyer and + Esra Erdem}, +title = {Unfounded Sets for Disjunctive Hybrid {MKNF} Knowledge Bases}, +booktitle = {Proceedings of the 18th International Conference on Principles of + Knowledge Representation and Reasoning, {KR} 2021, Online event, November + 3-12, 2021}, +pages = {432--441}, +year = {2021}, +doi = {10.24963/kr.2021/41}, +timestamp = {Wed, 03 Nov 2021 12:47:32 +0100}, +biburl = {https://dblp.org/rec/conf/kr/KillenY21.bib}, +bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{heyninckapproximation2021, +author = {Jesse Heyninck and + Ofer Arieli}, +editor = {Meghyn Bienvenu and + Gerhard Lakemeyer and + Esra Erdem}, +title = {Approximation Fixpoint Theory for Non-Deterministic Operators and + Its Application in Disjunctive Logic Programming}, +booktitle = {Proceedings of the 18th International Conference on Principles of + Knowledge Representation and Reasoning, {KR} 2021, Online event, November + 3-12, 2021}, +pages = {334--344}, +year = {2021}, +doi = {10.24963/kr.2021/32}, +timestamp = {Wed, 03 Nov 2021 12:47:32 +0100}, +biburl = {https://dblp.org/rec/conf/kr/HeyninckA21.bib}, +bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{kaminskiefficient2015, +author = {Tobias Kaminski and + Matthias Knorr and + Jo{\~{a}}o Leite}, +editor = {Qiang Yang and + Michael J. Wooldridge}, +title = {Efficient Paraconsistent Reasoning with Ontologies and Rules}, +booktitle = {Proceedings of the Twenty-Fourth International Joint Conference on + Artificial Intelligence, {IJCAI} 2015, Buenos Aires, Argentina, July + 25-31, 2015}, +pages = {3098--3105}, +publisher = {{AAAI} Press}, +year = {2015}, +url = {http://ijcai.org/Abstract/15/437}, +timestamp = {Wed, 23 Feb 2022 14:32:42 +0100}, +biburl = {https://dblp.org/rec/conf/ijcai/KaminskiKL15.bib}, +bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{headcycleisNP, +author = {Rachel Ben{-}Eliyahu and + Rina Dechter}, +title = {Propositional Semantics for Disjunctive Logic Programs}, +journal = {Ann. Math. Artif. Intell.}, +volume = {12}, +number = {1-2}, +pages = {53--87}, +year = {1994}, +doi = {10.1007/BF01530761}, +timestamp = {Sun, 28 May 2017 13:20:59 +0200}, +biburl = {https://dblp.org/rec/journals/amai/Ben-EliyahuD94.bib}, +bibsource = {dblp computer science bibliography, https://dblp.org} +} \ No newline at end of file diff --git a/grammars/HMKNF.interp b/grammars/HMKNF.interp new file mode 100644 index 0000000..9086cd4 --- /dev/null +++ b/grammars/HMKNF.interp @@ -0,0 +1,47 @@ +token literal names: +null +'.' +',' +':-' +'(' +')' +'-' +'|' +'&' +'->' +'not' +null +null +null + +token symbolic names: +null +null +null +null +null +null +null +null +null +null +null +COMMENT +WS +IDENTIFIER + +rule names: +kb +lrule +head +body +orule +oformula +katom +oatom +patom +natom + + +atn: +[4, 1, 13, 91, 2, 0, 7, 0, 2, 1, 7, 1, 2, 2, 7, 2, 2, 3, 7, 3, 2, 4, 7, 4, 2, 5, 7, 5, 2, 6, 7, 6, 2, 7, 7, 7, 2, 8, 7, 8, 2, 9, 7, 9, 1, 0, 1, 0, 5, 0, 23, 8, 0, 10, 0, 12, 0, 26, 9, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 33, 8, 1, 1, 1, 1, 1, 1, 2, 1, 2, 1, 2, 5, 2, 40, 8, 2, 10, 2, 12, 2, 43, 9, 2, 1, 3, 1, 3, 1, 3, 1, 3, 5, 3, 49, 8, 3, 10, 3, 12, 3, 52, 9, 3, 3, 3, 54, 8, 3, 1, 4, 1, 4, 1, 4, 1, 5, 1, 5, 1, 5, 1, 5, 1, 5, 1, 5, 1, 5, 1, 5, 3, 5, 67, 8, 5, 1, 5, 1, 5, 1, 5, 1, 5, 1, 5, 1, 5, 5, 5, 75, 8, 5, 10, 5, 12, 5, 78, 9, 5, 1, 6, 1, 6, 3, 6, 82, 8, 6, 1, 7, 1, 7, 1, 8, 1, 8, 1, 9, 1, 9, 1, 9, 1, 9, 0, 1, 10, 10, 0, 2, 4, 6, 8, 10, 12, 14, 16, 18, 0, 1, 1, 0, 7, 8, 92, 0, 24, 1, 0, 0, 0, 2, 32, 1, 0, 0, 0, 4, 36, 1, 0, 0, 0, 6, 44, 1, 0, 0, 0, 8, 55, 1, 0, 0, 0, 10, 66, 1, 0, 0, 0, 12, 81, 1, 0, 0, 0, 14, 83, 1, 0, 0, 0, 16, 85, 1, 0, 0, 0, 18, 87, 1, 0, 0, 0, 20, 23, 3, 2, 1, 0, 21, 23, 3, 8, 4, 0, 22, 20, 1, 0, 0, 0, 22, 21, 1, 0, 0, 0, 23, 26, 1, 0, 0, 0, 24, 22, 1, 0, 0, 0, 24, 25, 1, 0, 0, 0, 25, 1, 1, 0, 0, 0, 26, 24, 1, 0, 0, 0, 27, 28, 3, 4, 2, 0, 28, 29, 3, 6, 3, 0, 29, 33, 1, 0, 0, 0, 30, 33, 3, 4, 2, 0, 31, 33, 3, 6, 3, 0, 32, 27, 1, 0, 0, 0, 32, 30, 1, 0, 0, 0, 32, 31, 1, 0, 0, 0, 33, 34, 1, 0, 0, 0, 34, 35, 5, 1, 0, 0, 35, 3, 1, 0, 0, 0, 36, 41, 5, 13, 0, 0, 37, 38, 5, 2, 0, 0, 38, 40, 5, 13, 0, 0, 39, 37, 1, 0, 0, 0, 40, 43, 1, 0, 0, 0, 41, 39, 1, 0, 0, 0, 41, 42, 1, 0, 0, 0, 42, 5, 1, 0, 0, 0, 43, 41, 1, 0, 0, 0, 44, 53, 5, 3, 0, 0, 45, 50, 3, 12, 6, 0, 46, 47, 5, 2, 0, 0, 47, 49, 3, 12, 6, 0, 48, 46, 1, 0, 0, 0, 49, 52, 1, 0, 0, 0, 50, 48, 1, 0, 0, 0, 50, 51, 1, 0, 0, 0, 51, 54, 1, 0, 0, 0, 52, 50, 1, 0, 0, 0, 53, 45, 1, 0, 0, 0, 53, 54, 1, 0, 0, 0, 54, 7, 1, 0, 0, 0, 55, 56, 3, 10, 5, 0, 56, 57, 5, 1, 0, 0, 57, 9, 1, 0, 0, 0, 58, 59, 6, 5, -1, 0, 59, 60, 5, 4, 0, 0, 60, 61, 3, 10, 5, 0, 61, 62, 5, 5, 0, 0, 62, 67, 1, 0, 0, 0, 63, 67, 3, 14, 7, 0, 64, 65, 5, 6, 0, 0, 65, 67, 3, 10, 5, 3, 66, 58, 1, 0, 0, 0, 66, 63, 1, 0, 0, 0, 66, 64, 1, 0, 0, 0, 67, 76, 1, 0, 0, 0, 68, 69, 10, 2, 0, 0, 69, 70, 7, 0, 0, 0, 70, 75, 3, 10, 5, 3, 71, 72, 10, 1, 0, 0, 72, 73, 5, 9, 0, 0, 73, 75, 3, 10, 5, 1, 74, 68, 1, 0, 0, 0, 74, 71, 1, 0, 0, 0, 75, 78, 1, 0, 0, 0, 76, 74, 1, 0, 0, 0, 76, 77, 1, 0, 0, 0, 77, 11, 1, 0, 0, 0, 78, 76, 1, 0, 0, 0, 79, 82, 3, 16, 8, 0, 80, 82, 3, 18, 9, 0, 81, 79, 1, 0, 0, 0, 81, 80, 1, 0, 0, 0, 82, 13, 1, 0, 0, 0, 83, 84, 5, 13, 0, 0, 84, 15, 1, 0, 0, 0, 85, 86, 5, 13, 0, 0, 86, 17, 1, 0, 0, 0, 87, 88, 5, 10, 0, 0, 88, 89, 5, 13, 0, 0, 89, 19, 1, 0, 0, 0, 10, 22, 24, 32, 41, 50, 53, 66, 74, 76, 81] \ No newline at end of file diff --git a/grammars/HMKNF.tokens b/grammars/HMKNF.tokens new file mode 100644 index 0000000..fb3e177 --- /dev/null +++ b/grammars/HMKNF.tokens @@ -0,0 +1,23 @@ +T__0=1 +T__1=2 +T__2=3 +T__3=4 +T__4=5 +T__5=6 +T__6=7 +T__7=8 +T__8=9 +T__9=10 +COMMENT=11 +WS=12 +IDENTIFIER=13 +'.'=1 +','=2 +':-'=3 +'('=4 +')'=5 +'-'=6 +'|'=7 +'&'=8 +'->'=9 +'not'=10 diff --git a/grammars/HMKNFLexer.interp b/grammars/HMKNFLexer.interp new file mode 100644 index 0000000..10f5e8c --- /dev/null +++ b/grammars/HMKNFLexer.interp @@ -0,0 +1,56 @@ +token literal names: +null +'.' +',' +':-' +'(' +')' +'-' +'|' +'&' +'->' +'not' +null +null +null + +token symbolic names: +null +null +null +null +null +null +null +null +null +null +null +COMMENT +WS +IDENTIFIER + +rule names: +T__0 +T__1 +T__2 +T__3 +T__4 +T__5 +T__6 +T__7 +T__8 +T__9 +COMMENT +WS +IDENTIFIER + +channel names: +DEFAULT_TOKEN_CHANNEL +HIDDEN + +mode names: +DEFAULT_MODE + +atn: +[4, 0, 13, 76, 6, -1, 2, 0, 7, 0, 2, 1, 7, 1, 2, 2, 7, 2, 2, 3, 7, 3, 2, 4, 7, 4, 2, 5, 7, 5, 2, 6, 7, 6, 2, 7, 7, 7, 2, 8, 7, 8, 2, 9, 7, 9, 2, 10, 7, 10, 2, 11, 7, 11, 2, 12, 7, 12, 1, 0, 1, 0, 1, 1, 1, 1, 1, 2, 1, 2, 1, 2, 1, 3, 1, 3, 1, 4, 1, 4, 1, 5, 1, 5, 1, 6, 1, 6, 1, 7, 1, 7, 1, 8, 1, 8, 1, 8, 1, 9, 1, 9, 1, 9, 1, 9, 1, 10, 1, 10, 5, 10, 54, 8, 10, 10, 10, 12, 10, 57, 9, 10, 1, 10, 1, 10, 1, 10, 1, 10, 1, 11, 4, 11, 64, 8, 11, 11, 11, 12, 11, 65, 1, 11, 1, 11, 1, 12, 1, 12, 5, 12, 72, 8, 12, 10, 12, 12, 12, 75, 9, 12, 1, 55, 0, 13, 1, 1, 3, 2, 5, 3, 7, 4, 9, 5, 11, 6, 13, 7, 15, 8, 17, 9, 19, 10, 21, 11, 23, 12, 25, 13, 1, 0, 3, 3, 0, 9, 10, 13, 13, 32, 32, 2, 0, 39, 39, 97, 122, 5, 0, 39, 39, 48, 57, 65, 90, 95, 95, 97, 122, 78, 0, 1, 1, 0, 0, 0, 0, 3, 1, 0, 0, 0, 0, 5, 1, 0, 0, 0, 0, 7, 1, 0, 0, 0, 0, 9, 1, 0, 0, 0, 0, 11, 1, 0, 0, 0, 0, 13, 1, 0, 0, 0, 0, 15, 1, 0, 0, 0, 0, 17, 1, 0, 0, 0, 0, 19, 1, 0, 0, 0, 0, 21, 1, 0, 0, 0, 0, 23, 1, 0, 0, 0, 0, 25, 1, 0, 0, 0, 1, 27, 1, 0, 0, 0, 3, 29, 1, 0, 0, 0, 5, 31, 1, 0, 0, 0, 7, 34, 1, 0, 0, 0, 9, 36, 1, 0, 0, 0, 11, 38, 1, 0, 0, 0, 13, 40, 1, 0, 0, 0, 15, 42, 1, 0, 0, 0, 17, 44, 1, 0, 0, 0, 19, 47, 1, 0, 0, 0, 21, 51, 1, 0, 0, 0, 23, 63, 1, 0, 0, 0, 25, 69, 1, 0, 0, 0, 27, 28, 5, 46, 0, 0, 28, 2, 1, 0, 0, 0, 29, 30, 5, 44, 0, 0, 30, 4, 1, 0, 0, 0, 31, 32, 5, 58, 0, 0, 32, 33, 5, 45, 0, 0, 33, 6, 1, 0, 0, 0, 34, 35, 5, 40, 0, 0, 35, 8, 1, 0, 0, 0, 36, 37, 5, 41, 0, 0, 37, 10, 1, 0, 0, 0, 38, 39, 5, 45, 0, 0, 39, 12, 1, 0, 0, 0, 40, 41, 5, 124, 0, 0, 41, 14, 1, 0, 0, 0, 42, 43, 5, 38, 0, 0, 43, 16, 1, 0, 0, 0, 44, 45, 5, 45, 0, 0, 45, 46, 5, 62, 0, 0, 46, 18, 1, 0, 0, 0, 47, 48, 5, 110, 0, 0, 48, 49, 5, 111, 0, 0, 49, 50, 5, 116, 0, 0, 50, 20, 1, 0, 0, 0, 51, 55, 5, 35, 0, 0, 52, 54, 9, 0, 0, 0, 53, 52, 1, 0, 0, 0, 54, 57, 1, 0, 0, 0, 55, 56, 1, 0, 0, 0, 55, 53, 1, 0, 0, 0, 56, 58, 1, 0, 0, 0, 57, 55, 1, 0, 0, 0, 58, 59, 5, 10, 0, 0, 59, 60, 1, 0, 0, 0, 60, 61, 6, 10, 0, 0, 61, 22, 1, 0, 0, 0, 62, 64, 7, 0, 0, 0, 63, 62, 1, 0, 0, 0, 64, 65, 1, 0, 0, 0, 65, 63, 1, 0, 0, 0, 65, 66, 1, 0, 0, 0, 66, 67, 1, 0, 0, 0, 67, 68, 6, 11, 0, 0, 68, 24, 1, 0, 0, 0, 69, 73, 7, 1, 0, 0, 70, 72, 7, 2, 0, 0, 71, 70, 1, 0, 0, 0, 72, 75, 1, 0, 0, 0, 73, 71, 1, 0, 0, 0, 73, 74, 1, 0, 0, 0, 74, 26, 1, 0, 0, 0, 75, 73, 1, 0, 0, 0, 4, 0, 55, 65, 73, 1, 6, 0, 0] \ No newline at end of file diff --git a/grammars/HMKNFLexer.py b/grammars/HMKNFLexer.py new file mode 100644 index 0000000..3f19512 --- /dev/null +++ b/grammars/HMKNFLexer.py @@ -0,0 +1,84 @@ +# Generated from HMKNF.g4 by ANTLR 4.10.1 +from antlr4 import * +from io import StringIO +import sys +if sys.version_info[1] > 5: + from typing import TextIO +else: + from typing.io import TextIO + + +def serializedATN(): + return [ + 4,0,13,76,6,-1,2,0,7,0,2,1,7,1,2,2,7,2,2,3,7,3,2,4,7,4,2,5,7,5,2, + 6,7,6,2,7,7,7,2,8,7,8,2,9,7,9,2,10,7,10,2,11,7,11,2,12,7,12,1,0, + 1,0,1,1,1,1,1,2,1,2,1,2,1,3,1,3,1,4,1,4,1,5,1,5,1,6,1,6,1,7,1,7, + 1,8,1,8,1,8,1,9,1,9,1,9,1,9,1,10,1,10,5,10,54,8,10,10,10,12,10,57, + 9,10,1,10,1,10,1,10,1,10,1,11,4,11,64,8,11,11,11,12,11,65,1,11,1, + 11,1,12,1,12,5,12,72,8,12,10,12,12,12,75,9,12,1,55,0,13,1,1,3,2, + 5,3,7,4,9,5,11,6,13,7,15,8,17,9,19,10,21,11,23,12,25,13,1,0,3,3, + 0,9,10,13,13,32,32,2,0,39,39,97,122,5,0,39,39,48,57,65,90,95,95, + 97,122,78,0,1,1,0,0,0,0,3,1,0,0,0,0,5,1,0,0,0,0,7,1,0,0,0,0,9,1, + 0,0,0,0,11,1,0,0,0,0,13,1,0,0,0,0,15,1,0,0,0,0,17,1,0,0,0,0,19,1, + 0,0,0,0,21,1,0,0,0,0,23,1,0,0,0,0,25,1,0,0,0,1,27,1,0,0,0,3,29,1, + 0,0,0,5,31,1,0,0,0,7,34,1,0,0,0,9,36,1,0,0,0,11,38,1,0,0,0,13,40, + 1,0,0,0,15,42,1,0,0,0,17,44,1,0,0,0,19,47,1,0,0,0,21,51,1,0,0,0, + 23,63,1,0,0,0,25,69,1,0,0,0,27,28,5,46,0,0,28,2,1,0,0,0,29,30,5, + 44,0,0,30,4,1,0,0,0,31,32,5,58,0,0,32,33,5,45,0,0,33,6,1,0,0,0,34, + 35,5,40,0,0,35,8,1,0,0,0,36,37,5,41,0,0,37,10,1,0,0,0,38,39,5,45, + 0,0,39,12,1,0,0,0,40,41,5,124,0,0,41,14,1,0,0,0,42,43,5,38,0,0,43, + 16,1,0,0,0,44,45,5,45,0,0,45,46,5,62,0,0,46,18,1,0,0,0,47,48,5,110, + 0,0,48,49,5,111,0,0,49,50,5,116,0,0,50,20,1,0,0,0,51,55,5,35,0,0, + 52,54,9,0,0,0,53,52,1,0,0,0,54,57,1,0,0,0,55,56,1,0,0,0,55,53,1, + 0,0,0,56,58,1,0,0,0,57,55,1,0,0,0,58,59,5,10,0,0,59,60,1,0,0,0,60, + 61,6,10,0,0,61,22,1,0,0,0,62,64,7,0,0,0,63,62,1,0,0,0,64,65,1,0, + 0,0,65,63,1,0,0,0,65,66,1,0,0,0,66,67,1,0,0,0,67,68,6,11,0,0,68, + 24,1,0,0,0,69,73,7,1,0,0,70,72,7,2,0,0,71,70,1,0,0,0,72,75,1,0,0, + 0,73,71,1,0,0,0,73,74,1,0,0,0,74,26,1,0,0,0,75,73,1,0,0,0,4,0,55, + 65,73,1,6,0,0 + ] + +class HMKNFLexer(Lexer): + + atn = ATNDeserializer().deserialize(serializedATN()) + + decisionsToDFA = [ DFA(ds, i) for i, ds in enumerate(atn.decisionToState) ] + + T__0 = 1 + T__1 = 2 + T__2 = 3 + T__3 = 4 + T__4 = 5 + T__5 = 6 + T__6 = 7 + T__7 = 8 + T__8 = 9 + T__9 = 10 + COMMENT = 11 + WS = 12 + IDENTIFIER = 13 + + channelNames = [ u"DEFAULT_TOKEN_CHANNEL", u"HIDDEN" ] + + modeNames = [ "DEFAULT_MODE" ] + + literalNames = [ "", + "'.'", "','", "':-'", "'('", "')'", "'-'", "'|'", "'&'", "'->'", + "'not'" ] + + symbolicNames = [ "", + "COMMENT", "WS", "IDENTIFIER" ] + + ruleNames = [ "T__0", "T__1", "T__2", "T__3", "T__4", "T__5", "T__6", + "T__7", "T__8", "T__9", "COMMENT", "WS", "IDENTIFIER" ] + + grammarFileName = "HMKNF.g4" + + def __init__(self, input=None, output:TextIO = sys.stdout): + super().__init__(input, output) + self.checkVersion("4.10.1") + self._interp = LexerATNSimulator(self, self.atn, self.decisionsToDFA, PredictionContextCache()) + self._actions = None + self._predicates = None + + diff --git a/grammars/HMKNFLexer.tokens b/grammars/HMKNFLexer.tokens new file mode 100644 index 0000000..fb3e177 --- /dev/null +++ b/grammars/HMKNFLexer.tokens @@ -0,0 +1,23 @@ +T__0=1 +T__1=2 +T__2=3 +T__3=4 +T__4=5 +T__5=6 +T__6=7 +T__7=8 +T__8=9 +T__9=10 +COMMENT=11 +WS=12 +IDENTIFIER=13 +'.'=1 +','=2 +':-'=3 +'('=4 +')'=5 +'-'=6 +'|'=7 +'&'=8 +'->'=9 +'not'=10 diff --git a/grammars/HMKNFParser.py b/grammars/HMKNFParser.py new file mode 100644 index 0000000..1815a70 --- /dev/null +++ b/grammars/HMKNFParser.py @@ -0,0 +1,806 @@ +# Generated from HMKNF.g4 by ANTLR 4.10.1 +# encoding: utf-8 +from antlr4 import * +from io import StringIO +import sys +if sys.version_info[1] > 5: + from typing import TextIO +else: + from typing.io import TextIO + +def serializedATN(): + return [ + 4,1,13,91,2,0,7,0,2,1,7,1,2,2,7,2,2,3,7,3,2,4,7,4,2,5,7,5,2,6,7, + 6,2,7,7,7,2,8,7,8,2,9,7,9,1,0,1,0,5,0,23,8,0,10,0,12,0,26,9,0,1, + 1,1,1,1,1,1,1,1,1,3,1,33,8,1,1,1,1,1,1,2,1,2,1,2,5,2,40,8,2,10,2, + 12,2,43,9,2,1,3,1,3,1,3,1,3,5,3,49,8,3,10,3,12,3,52,9,3,3,3,54,8, + 3,1,4,1,4,1,4,1,5,1,5,1,5,1,5,1,5,1,5,1,5,1,5,3,5,67,8,5,1,5,1,5, + 1,5,1,5,1,5,1,5,5,5,75,8,5,10,5,12,5,78,9,5,1,6,1,6,3,6,82,8,6,1, + 7,1,7,1,8,1,8,1,9,1,9,1,9,1,9,0,1,10,10,0,2,4,6,8,10,12,14,16,18, + 0,1,1,0,7,8,92,0,24,1,0,0,0,2,32,1,0,0,0,4,36,1,0,0,0,6,44,1,0,0, + 0,8,55,1,0,0,0,10,66,1,0,0,0,12,81,1,0,0,0,14,83,1,0,0,0,16,85,1, + 0,0,0,18,87,1,0,0,0,20,23,3,2,1,0,21,23,3,8,4,0,22,20,1,0,0,0,22, + 21,1,0,0,0,23,26,1,0,0,0,24,22,1,0,0,0,24,25,1,0,0,0,25,1,1,0,0, + 0,26,24,1,0,0,0,27,28,3,4,2,0,28,29,3,6,3,0,29,33,1,0,0,0,30,33, + 3,4,2,0,31,33,3,6,3,0,32,27,1,0,0,0,32,30,1,0,0,0,32,31,1,0,0,0, + 33,34,1,0,0,0,34,35,5,1,0,0,35,3,1,0,0,0,36,41,5,13,0,0,37,38,5, + 2,0,0,38,40,5,13,0,0,39,37,1,0,0,0,40,43,1,0,0,0,41,39,1,0,0,0,41, + 42,1,0,0,0,42,5,1,0,0,0,43,41,1,0,0,0,44,53,5,3,0,0,45,50,3,12,6, + 0,46,47,5,2,0,0,47,49,3,12,6,0,48,46,1,0,0,0,49,52,1,0,0,0,50,48, + 1,0,0,0,50,51,1,0,0,0,51,54,1,0,0,0,52,50,1,0,0,0,53,45,1,0,0,0, + 53,54,1,0,0,0,54,7,1,0,0,0,55,56,3,10,5,0,56,57,5,1,0,0,57,9,1,0, + 0,0,58,59,6,5,-1,0,59,60,5,4,0,0,60,61,3,10,5,0,61,62,5,5,0,0,62, + 67,1,0,0,0,63,67,3,14,7,0,64,65,5,6,0,0,65,67,3,10,5,3,66,58,1,0, + 0,0,66,63,1,0,0,0,66,64,1,0,0,0,67,76,1,0,0,0,68,69,10,2,0,0,69, + 70,7,0,0,0,70,75,3,10,5,3,71,72,10,1,0,0,72,73,5,9,0,0,73,75,3,10, + 5,1,74,68,1,0,0,0,74,71,1,0,0,0,75,78,1,0,0,0,76,74,1,0,0,0,76,77, + 1,0,0,0,77,11,1,0,0,0,78,76,1,0,0,0,79,82,3,16,8,0,80,82,3,18,9, + 0,81,79,1,0,0,0,81,80,1,0,0,0,82,13,1,0,0,0,83,84,5,13,0,0,84,15, + 1,0,0,0,85,86,5,13,0,0,86,17,1,0,0,0,87,88,5,10,0,0,88,89,5,13,0, + 0,89,19,1,0,0,0,10,22,24,32,41,50,53,66,74,76,81 + ] + +class HMKNFParser ( Parser ): + + grammarFileName = "HMKNF.g4" + + atn = ATNDeserializer().deserialize(serializedATN()) + + decisionsToDFA = [ DFA(ds, i) for i, ds in enumerate(atn.decisionToState) ] + + sharedContextCache = PredictionContextCache() + + literalNames = [ "", "'.'", "','", "':-'", "'('", "')'", "'-'", + "'|'", "'&'", "'->'", "'not'" ] + + symbolicNames = [ "", "", "", "", + "", "", "", "", + "", "", "", "COMMENT", + "WS", "IDENTIFIER" ] + + RULE_kb = 0 + RULE_lrule = 1 + RULE_head = 2 + RULE_body = 3 + RULE_orule = 4 + RULE_oformula = 5 + RULE_katom = 6 + RULE_oatom = 7 + RULE_patom = 8 + RULE_natom = 9 + + ruleNames = [ "kb", "lrule", "head", "body", "orule", "oformula", "katom", + "oatom", "patom", "natom" ] + + EOF = Token.EOF + T__0=1 + T__1=2 + T__2=3 + T__3=4 + T__4=5 + T__5=6 + T__6=7 + T__7=8 + T__8=9 + T__9=10 + COMMENT=11 + WS=12 + IDENTIFIER=13 + + def __init__(self, input:TokenStream, output:TextIO = sys.stdout): + super().__init__(input, output) + self.checkVersion("4.10.1") + self._interp = ParserATNSimulator(self, self.atn, self.decisionsToDFA, self.sharedContextCache) + self._predicates = None + + + + + class KbContext(ParserRuleContext): + __slots__ = 'parser' + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def lrule(self, i:int=None): + if i is None: + return self.getTypedRuleContexts(HMKNFParser.LruleContext) + else: + return self.getTypedRuleContext(HMKNFParser.LruleContext,i) + + + def orule(self, i:int=None): + if i is None: + return self.getTypedRuleContexts(HMKNFParser.OruleContext) + else: + return self.getTypedRuleContext(HMKNFParser.OruleContext,i) + + + def getRuleIndex(self): + return HMKNFParser.RULE_kb + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitKb" ): + return visitor.visitKb(self) + else: + return visitor.visitChildren(self) + + + + + def kb(self): + + localctx = HMKNFParser.KbContext(self, self._ctx, self.state) + self.enterRule(localctx, 0, self.RULE_kb) + self._la = 0 # Token type + try: + self.enterOuterAlt(localctx, 1) + self.state = 24 + self._errHandler.sync(self) + _la = self._input.LA(1) + while (((_la) & ~0x3f) == 0 and ((1 << _la) & ((1 << HMKNFParser.T__2) | (1 << HMKNFParser.T__3) | (1 << HMKNFParser.T__5) | (1 << HMKNFParser.IDENTIFIER))) != 0): + self.state = 22 + self._errHandler.sync(self) + la_ = self._interp.adaptivePredict(self._input,0,self._ctx) + if la_ == 1: + self.state = 20 + self.lrule() + pass + + elif la_ == 2: + self.state = 21 + self.orule() + pass + + + self.state = 26 + self._errHandler.sync(self) + _la = self._input.LA(1) + + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + + class LruleContext(ParserRuleContext): + __slots__ = 'parser' + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def head(self): + return self.getTypedRuleContext(HMKNFParser.HeadContext,0) + + + def body(self): + return self.getTypedRuleContext(HMKNFParser.BodyContext,0) + + + def getRuleIndex(self): + return HMKNFParser.RULE_lrule + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitLrule" ): + return visitor.visitLrule(self) + else: + return visitor.visitChildren(self) + + + + + def lrule(self): + + localctx = HMKNFParser.LruleContext(self, self._ctx, self.state) + self.enterRule(localctx, 2, self.RULE_lrule) + try: + self.enterOuterAlt(localctx, 1) + self.state = 32 + self._errHandler.sync(self) + la_ = self._interp.adaptivePredict(self._input,2,self._ctx) + if la_ == 1: + self.state = 27 + self.head() + self.state = 28 + self.body() + pass + + elif la_ == 2: + self.state = 30 + self.head() + pass + + elif la_ == 3: + self.state = 31 + self.body() + pass + + + self.state = 34 + self.match(HMKNFParser.T__0) + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + + class HeadContext(ParserRuleContext): + __slots__ = 'parser' + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def IDENTIFIER(self, i:int=None): + if i is None: + return self.getTokens(HMKNFParser.IDENTIFIER) + else: + return self.getToken(HMKNFParser.IDENTIFIER, i) + + def getRuleIndex(self): + return HMKNFParser.RULE_head + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitHead" ): + return visitor.visitHead(self) + else: + return visitor.visitChildren(self) + + + + + def head(self): + + localctx = HMKNFParser.HeadContext(self, self._ctx, self.state) + self.enterRule(localctx, 4, self.RULE_head) + self._la = 0 # Token type + try: + self.enterOuterAlt(localctx, 1) + self.state = 36 + self.match(HMKNFParser.IDENTIFIER) + self.state = 41 + self._errHandler.sync(self) + _la = self._input.LA(1) + while _la==HMKNFParser.T__1: + self.state = 37 + self.match(HMKNFParser.T__1) + self.state = 38 + self.match(HMKNFParser.IDENTIFIER) + self.state = 43 + self._errHandler.sync(self) + _la = self._input.LA(1) + + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + + class BodyContext(ParserRuleContext): + __slots__ = 'parser' + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def katom(self, i:int=None): + if i is None: + return self.getTypedRuleContexts(HMKNFParser.KatomContext) + else: + return self.getTypedRuleContext(HMKNFParser.KatomContext,i) + + + def getRuleIndex(self): + return HMKNFParser.RULE_body + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitBody" ): + return visitor.visitBody(self) + else: + return visitor.visitChildren(self) + + + + + def body(self): + + localctx = HMKNFParser.BodyContext(self, self._ctx, self.state) + self.enterRule(localctx, 6, self.RULE_body) + self._la = 0 # Token type + try: + self.enterOuterAlt(localctx, 1) + self.state = 44 + self.match(HMKNFParser.T__2) + self.state = 53 + self._errHandler.sync(self) + _la = self._input.LA(1) + if _la==HMKNFParser.T__9 or _la==HMKNFParser.IDENTIFIER: + self.state = 45 + self.katom() + self.state = 50 + self._errHandler.sync(self) + _la = self._input.LA(1) + while _la==HMKNFParser.T__1: + self.state = 46 + self.match(HMKNFParser.T__1) + self.state = 47 + self.katom() + self.state = 52 + self._errHandler.sync(self) + _la = self._input.LA(1) + + + + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + + class OruleContext(ParserRuleContext): + __slots__ = 'parser' + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def oformula(self): + return self.getTypedRuleContext(HMKNFParser.OformulaContext,0) + + + def getRuleIndex(self): + return HMKNFParser.RULE_orule + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitOrule" ): + return visitor.visitOrule(self) + else: + return visitor.visitChildren(self) + + + + + def orule(self): + + localctx = HMKNFParser.OruleContext(self, self._ctx, self.state) + self.enterRule(localctx, 8, self.RULE_orule) + try: + self.enterOuterAlt(localctx, 1) + self.state = 55 + self.oformula(0) + self.state = 56 + self.match(HMKNFParser.T__0) + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + + class OformulaContext(ParserRuleContext): + __slots__ = 'parser' + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + + def getRuleIndex(self): + return HMKNFParser.RULE_oformula + + + def copyFrom(self, ctx:ParserRuleContext): + super().copyFrom(ctx) + + + class NegationContext(OformulaContext): + + def __init__(self, parser, ctx:ParserRuleContext): # actually a HMKNFParser.OformulaContext + super().__init__(parser) + self.copyFrom(ctx) + + def oformula(self): + return self.getTypedRuleContext(HMKNFParser.OformulaContext,0) + + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitNegation" ): + return visitor.visitNegation(self) + else: + return visitor.visitChildren(self) + + + class DisjOrConjContext(OformulaContext): + + def __init__(self, parser, ctx:ParserRuleContext): # actually a HMKNFParser.OformulaContext + super().__init__(parser) + self.operator = None # Token + self.copyFrom(ctx) + + def oformula(self, i:int=None): + if i is None: + return self.getTypedRuleContexts(HMKNFParser.OformulaContext) + else: + return self.getTypedRuleContext(HMKNFParser.OformulaContext,i) + + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitDisjOrConj" ): + return visitor.visitDisjOrConj(self) + else: + return visitor.visitChildren(self) + + + class ParenthContext(OformulaContext): + + def __init__(self, parser, ctx:ParserRuleContext): # actually a HMKNFParser.OformulaContext + super().__init__(parser) + self.copyFrom(ctx) + + def oformula(self): + return self.getTypedRuleContext(HMKNFParser.OformulaContext,0) + + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitParenth" ): + return visitor.visitParenth(self) + else: + return visitor.visitChildren(self) + + + class ImpContext(OformulaContext): + + def __init__(self, parser, ctx:ParserRuleContext): # actually a HMKNFParser.OformulaContext + super().__init__(parser) + self.copyFrom(ctx) + + def oformula(self, i:int=None): + if i is None: + return self.getTypedRuleContexts(HMKNFParser.OformulaContext) + else: + return self.getTypedRuleContext(HMKNFParser.OformulaContext,i) + + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitImp" ): + return visitor.visitImp(self) + else: + return visitor.visitChildren(self) + + + class LiteralContext(OformulaContext): + + def __init__(self, parser, ctx:ParserRuleContext): # actually a HMKNFParser.OformulaContext + super().__init__(parser) + self.copyFrom(ctx) + + def oatom(self): + return self.getTypedRuleContext(HMKNFParser.OatomContext,0) + + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitLiteral" ): + return visitor.visitLiteral(self) + else: + return visitor.visitChildren(self) + + + + def oformula(self, _p:int=0): + _parentctx = self._ctx + _parentState = self.state + localctx = HMKNFParser.OformulaContext(self, self._ctx, _parentState) + _prevctx = localctx + _startState = 10 + self.enterRecursionRule(localctx, 10, self.RULE_oformula, _p) + self._la = 0 # Token type + try: + self.enterOuterAlt(localctx, 1) + self.state = 66 + self._errHandler.sync(self) + token = self._input.LA(1) + if token in [HMKNFParser.T__3]: + localctx = HMKNFParser.ParenthContext(self, localctx) + self._ctx = localctx + _prevctx = localctx + + self.state = 59 + self.match(HMKNFParser.T__3) + self.state = 60 + self.oformula(0) + self.state = 61 + self.match(HMKNFParser.T__4) + pass + elif token in [HMKNFParser.IDENTIFIER]: + localctx = HMKNFParser.LiteralContext(self, localctx) + self._ctx = localctx + _prevctx = localctx + self.state = 63 + self.oatom() + pass + elif token in [HMKNFParser.T__5]: + localctx = HMKNFParser.NegationContext(self, localctx) + self._ctx = localctx + _prevctx = localctx + self.state = 64 + self.match(HMKNFParser.T__5) + self.state = 65 + self.oformula(3) + pass + else: + raise NoViableAltException(self) + + self._ctx.stop = self._input.LT(-1) + self.state = 76 + self._errHandler.sync(self) + _alt = self._interp.adaptivePredict(self._input,8,self._ctx) + while _alt!=2 and _alt!=ATN.INVALID_ALT_NUMBER: + if _alt==1: + if self._parseListeners is not None: + self.triggerExitRuleEvent() + _prevctx = localctx + self.state = 74 + self._errHandler.sync(self) + la_ = self._interp.adaptivePredict(self._input,7,self._ctx) + if la_ == 1: + localctx = HMKNFParser.DisjOrConjContext(self, HMKNFParser.OformulaContext(self, _parentctx, _parentState)) + self.pushNewRecursionContext(localctx, _startState, self.RULE_oformula) + self.state = 68 + if not self.precpred(self._ctx, 2): + from antlr4.error.Errors import FailedPredicateException + raise FailedPredicateException(self, "self.precpred(self._ctx, 2)") + + self.state = 69 + localctx.operator = self._input.LT(1) + _la = self._input.LA(1) + if not(_la==HMKNFParser.T__6 or _la==HMKNFParser.T__7): + localctx.operator = self._errHandler.recoverInline(self) + else: + self._errHandler.reportMatch(self) + self.consume() + self.state = 70 + self.oformula(3) + pass + + elif la_ == 2: + localctx = HMKNFParser.ImpContext(self, HMKNFParser.OformulaContext(self, _parentctx, _parentState)) + self.pushNewRecursionContext(localctx, _startState, self.RULE_oformula) + self.state = 71 + if not self.precpred(self._ctx, 1): + from antlr4.error.Errors import FailedPredicateException + raise FailedPredicateException(self, "self.precpred(self._ctx, 1)") + self.state = 72 + self.match(HMKNFParser.T__8) + self.state = 73 + self.oformula(1) + pass + + + self.state = 78 + self._errHandler.sync(self) + _alt = self._interp.adaptivePredict(self._input,8,self._ctx) + + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.unrollRecursionContexts(_parentctx) + return localctx + + + class KatomContext(ParserRuleContext): + __slots__ = 'parser' + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def patom(self): + return self.getTypedRuleContext(HMKNFParser.PatomContext,0) + + + def natom(self): + return self.getTypedRuleContext(HMKNFParser.NatomContext,0) + + + def getRuleIndex(self): + return HMKNFParser.RULE_katom + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitKatom" ): + return visitor.visitKatom(self) + else: + return visitor.visitChildren(self) + + + + + def katom(self): + + localctx = HMKNFParser.KatomContext(self, self._ctx, self.state) + self.enterRule(localctx, 12, self.RULE_katom) + try: + self.state = 81 + self._errHandler.sync(self) + token = self._input.LA(1) + if token in [HMKNFParser.IDENTIFIER]: + self.enterOuterAlt(localctx, 1) + self.state = 79 + self.patom() + pass + elif token in [HMKNFParser.T__9]: + self.enterOuterAlt(localctx, 2) + self.state = 80 + self.natom() + pass + else: + raise NoViableAltException(self) + + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + + class OatomContext(ParserRuleContext): + __slots__ = 'parser' + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def IDENTIFIER(self): + return self.getToken(HMKNFParser.IDENTIFIER, 0) + + def getRuleIndex(self): + return HMKNFParser.RULE_oatom + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitOatom" ): + return visitor.visitOatom(self) + else: + return visitor.visitChildren(self) + + + + + def oatom(self): + + localctx = HMKNFParser.OatomContext(self, self._ctx, self.state) + self.enterRule(localctx, 14, self.RULE_oatom) + try: + self.enterOuterAlt(localctx, 1) + self.state = 83 + self.match(HMKNFParser.IDENTIFIER) + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + + class PatomContext(ParserRuleContext): + __slots__ = 'parser' + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def IDENTIFIER(self): + return self.getToken(HMKNFParser.IDENTIFIER, 0) + + def getRuleIndex(self): + return HMKNFParser.RULE_patom + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitPatom" ): + return visitor.visitPatom(self) + else: + return visitor.visitChildren(self) + + + + + def patom(self): + + localctx = HMKNFParser.PatomContext(self, self._ctx, self.state) + self.enterRule(localctx, 16, self.RULE_patom) + try: + self.enterOuterAlt(localctx, 1) + self.state = 85 + self.match(HMKNFParser.IDENTIFIER) + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + + class NatomContext(ParserRuleContext): + __slots__ = 'parser' + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def IDENTIFIER(self): + return self.getToken(HMKNFParser.IDENTIFIER, 0) + + def getRuleIndex(self): + return HMKNFParser.RULE_natom + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitNatom" ): + return visitor.visitNatom(self) + else: + return visitor.visitChildren(self) + + + + + def natom(self): + + localctx = HMKNFParser.NatomContext(self, self._ctx, self.state) + self.enterRule(localctx, 18, self.RULE_natom) + try: + self.enterOuterAlt(localctx, 1) + self.state = 87 + self.match(HMKNFParser.T__9) + self.state = 88 + self.match(HMKNFParser.IDENTIFIER) + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + + + def sempred(self, localctx:RuleContext, ruleIndex:int, predIndex:int): + if self._predicates == None: + self._predicates = dict() + self._predicates[5] = self.oformula_sempred + pred = self._predicates.get(ruleIndex, None) + if pred is None: + raise Exception("No predicate with index:" + str(ruleIndex)) + else: + return pred(localctx, predIndex) + + def oformula_sempred(self, localctx:OformulaContext, predIndex:int): + if predIndex == 0: + return self.precpred(self._ctx, 2) + + + if predIndex == 1: + return self.precpred(self._ctx, 1) + + + + + diff --git a/grammars/HMKNFVisitor.py b/grammars/HMKNFVisitor.py new file mode 100644 index 0000000..72283c8 --- /dev/null +++ b/grammars/HMKNFVisitor.py @@ -0,0 +1,83 @@ +# Generated from HMKNF.g4 by ANTLR 4.10.1 +from antlr4 import * +if __name__ is not None and "." in __name__: + from .HMKNFParser import HMKNFParser +else: + from HMKNFParser import HMKNFParser + +# This class defines a complete generic visitor for a parse tree produced by HMKNFParser. + +class HMKNFVisitor(ParseTreeVisitor): + + # Visit a parse tree produced by HMKNFParser#kb. + def visitKb(self, ctx:HMKNFParser.KbContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by HMKNFParser#lrule. + def visitLrule(self, ctx:HMKNFParser.LruleContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by HMKNFParser#head. + def visitHead(self, ctx:HMKNFParser.HeadContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by HMKNFParser#body. + def visitBody(self, ctx:HMKNFParser.BodyContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by HMKNFParser#orule. + def visitOrule(self, ctx:HMKNFParser.OruleContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by HMKNFParser#negation. + def visitNegation(self, ctx:HMKNFParser.NegationContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by HMKNFParser#disjOrConj. + def visitDisjOrConj(self, ctx:HMKNFParser.DisjOrConjContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by HMKNFParser#parenth. + def visitParenth(self, ctx:HMKNFParser.ParenthContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by HMKNFParser#imp. + def visitImp(self, ctx:HMKNFParser.ImpContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by HMKNFParser#literal. + def visitLiteral(self, ctx:HMKNFParser.LiteralContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by HMKNFParser#katom. + def visitKatom(self, ctx:HMKNFParser.KatomContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by HMKNFParser#oatom. + def visitOatom(self, ctx:HMKNFParser.OatomContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by HMKNFParser#patom. + def visitPatom(self, ctx:HMKNFParser.PatomContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by HMKNFParser#natom. + def visitNatom(self, ctx:HMKNFParser.NatomContext): + return self.visitChildren(ctx) + + + +del HMKNFParser \ No newline at end of file diff --git a/grammars/__init__.py b/grammars/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/hmknf.py b/hmknf.py new file mode 100644 index 0000000..f32a936 --- /dev/null +++ b/hmknf.py @@ -0,0 +1,64 @@ +from AST import ONegation, OFormula, OBinary, OAtom, OConst, KB, atom, Set +from more_itertools import powerset + + +def oformula_sat(o: OFormula, total_I: Set[atom]): + match o: + case OConst.TRUE: + return True + case OConst.FALSE: + return False + case OBinary("|", left, right): + return oformula_sat(left, total_I) or oformula_sat(right, total_I) + case OBinary("&", left, right): + return oformula_sat(left, total_I) and oformula_sat(right, total_I) + case OBinary("->", left, right): + return (not oformula_sat(left, total_I)) or oformula_sat(right, total_I) + case OAtom(name): + return name in total_I + case ONegation(of): + return not oformula_sat(of, total_I) + case _: + raise Exception("Ontology error") + + +def objective_knowledge_consistent(kb: KB, T: Set[atom], F: Set[atom]) -> bool: + "OB_{T, F} has at least one model" + undefined_atoms = (kb.katoms | kb.oatoms) - (T | F) + for I in powerset(undefined_atoms): + total_I = T.union(I) + if oformula_sat(kb.ont, total_I): + return True + return False + + +def objective_knowledge( + kb: KB, T: Set[atom], F: Set[atom] +) -> tuple[bool, Set[atom], Set[atom]]: + "OB_{T, F} |= a" + undefined_atoms = (kb.katoms | kb.oatoms) - (T | F) + entailed = kb.katoms + entailed_false = kb.katoms + consistent = False + for I in powerset(undefined_atoms): + total_I = T.union(I) + if oformula_sat(kb.ont, total_I): + consistent = True + entailed = entailed.intersection(total_I) + entailed_false = entailed_false.intersection(kb.katoms.difference(total_I)) + return consistent, T.union(entailed), F.union(entailed_false) + + +def objective_knowledge_brave(kb: KB, T: Set[atom], F: Set[atom]): + "OB_{T, F} |/= -a" + undefined_atoms = (kb.katoms | kb.oatoms) - (T | F) + entailed = Set() + entailed_false = Set() + consistent = False + for I in powerset(undefined_atoms): + total_I = T.union(I) + if oformula_sat(kb.ont, total_I): + consistent = True + entailed = entailed.union(total_I) + entailed_false = entailed_false.union(kb.katoms.difference(total_I)) + return consistent, T.union(entailed), F.union(entailed_false) diff --git a/knowledge_bases/simple.hmknf b/knowledge_bases/simple.hmknf new file mode 100644 index 0000000..0236f7c --- /dev/null +++ b/knowledge_bases/simple.hmknf @@ -0,0 +1,3 @@ +-b. +a :- not b. +b :- not a. diff --git a/knowledge_bases/simple2.hmknf b/knowledge_bases/simple2.hmknf new file mode 100644 index 0000000..7e98533 --- /dev/null +++ b/knowledge_bases/simple2.hmknf @@ -0,0 +1,4 @@ +:- c. +:- b. +:- a. +a. diff --git a/requirements.txt b/requirements.txt new file mode 100644 index 0000000..a68791d --- /dev/null +++ b/requirements.txt @@ -0,0 +1,3 @@ +antlr4-python3-runtime==4.10 +more-itertools==8.11.0 +black==23.3.0 diff --git a/solver.py b/solver.py new file mode 100755 index 0000000..921a860 --- /dev/null +++ b/solver.py @@ -0,0 +1,56 @@ +#!/usr/bin/env python3 +""" +An enumerative solver that will give all MKNF models of a given knowledge base + +usage: python solver.py knowledge_bases/simple.hmknf +OR +usage: python solver.py < knowledge_bases/simple.hmknf +""" + +from sys import argv, flags, stdin +from typing import Iterable + +from more_itertools import peekable + +from AST import loadProgram, atom, Set, KB +from aft import Kinterp, add_immediate_XY, fixpoint, stable_revision +from util import printp, powerset + + +def solver(kb: KB) -> Iterable[Kinterp]: + for T in powerset(kb.katoms): + for U in powerset(kb.katoms - T): + P = T | U + if verify(kb, T, P): + yield (T, P) + + +def verify(kb: KB, T: Set[atom], P: Set[atom]) -> bool: + "Return whether (T, P) corresponds to an MKNF model of kb" + Tp, Pp = stable_revision(kb, T, P) + if (Tp, Pp) != (T, P): + return False + + def check_rules(P: Set[atom]): + return add_immediate_XY(kb, P, T) + + return fixpoint(check_rules, Set()) == P + + +def main(): + if len(argv) > 1: + in_file = open(argv[1], "rt", encoding="utf8") + else: + in_file = stdin + kb = loadProgram(in_file.read()) + models = peekable(solver(kb)) + try: + models.peek() + except StopIteration: + print("no models") + for T, P in models: + printp(T, P) + + +if __name__ == "__main__" and not flags.interactive: + main() diff --git a/util.py b/util.py new file mode 100644 index 0000000..c3f6a5c --- /dev/null +++ b/util.py @@ -0,0 +1,64 @@ +from functools import wraps +from AST import Set, atom +import more_itertools + +def powerset(items): + return map(Set, more_itertools.powerset(items)) + + +def format_set(s: Set[atom]): + return "{" + ", ".join(sorted(s)) + "}" + + +def printp(*args): + whole = "(" + sets = (format_set(arg) for arg in args) + whole += ", ".join(sets) + whole += ")" + print(whole) + + +def prints_input(*pos): + def wrappest(fn): + @wraps(fn) + def wrapper(*args, **kwargs): + output = fn(*args, **kwargs) + print( + f"Input of {fn.__name__} pos: {pos}:", + " ".join( + (format_set(arg) if isinstance(arg, Set) else str(arg)) + for i, arg in enumerate(args) + if i in pos + ), + ) + return output + + return wrapper + + return wrappest + + +def prints_output(fn): + @wraps(fn) + def wrapper(*args, **kwargs): + output = fn(*args, **kwargs) + print( + f"Output of {fn.__name__}:", + format_set(output) if isinstance(output, Set) else output, + ) + return output + + return wrapper + + +def disabled_static(return_value): + "Disables a function by making it return a specified value instead" + + def wrappest(fn): + @wraps(fn) + def wrapper(*args, **kwargs): + return return_value + + return wrapper + + return wrappest