Provides a prolog database replacement that uses an interpretation of KIF

Logicmoo Project PrologMUD: A MUD server written in Prolog Maintainer: Douglas Miles Dec 13, 2035

Compute normal forms for SHOIQ formulae. Skolemize SHOI<Q> formula.

This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.

You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.

References

[1] Planning with First-Order Temporally Extended Goals Using Heuristic Search, Baier, J. and McIlraith, S., 2006. Proceedings of the 21st National Conference on Artificial Intelligence (AAAI06), July, Boston, MA

FORMULA SYNTAX

~( A) &(F, F) v(F, F) '=>'(F, F) '<=>'(F, F) all(X,A) exists(X,A) atleast(X,N,A) atmost(X,N,A)

Expressions

A BNF grammar for Expresions is the following:

BEXPR ::= <fluent-term> | ~(FACT) | FACT BEXPR ::= or(BEXPR,BEXPR) | and(BEXPR,BEXPR) | not(BEXPR)

Temporal Boolean Expressions

BNF grammar:

is_kif_string(?String) is det: If Is A Knowledge Interchange Format String.
convert_if_kif_string(?I, ?O) is det: Convert If Knowledge Interchange Format String.
from_kif_string(?String, ?Forms) is det: Converted From Knowledge Interchange Format String.
to_poss(KB, ?BDT, ?BDT) is det: Converted To Possibility.
nnf(+KB, +Fml, ?NNF) is det: Negated Normal Form.
is_skolem_setting(?S) is det: If Is A Skolem Setting.
get_quantifier_isa(?VALUE1, ?VALUE2, ?VALUE3) is det: get quantifier (isa/2).
logically_matches(?KB, ?A, ?B) is det: Logically Matches.
nnf(KB, +Fml, +FreeV, -NNF, -Paths) is det: Fml,NNF: See above. FreeV: List of free variables in Fml. Paths: Number of disjunctive paths in Fml.
axiom_lhs_to_rhs(?KB, :LHS, :RHS) is det: Axiom Left-hand-side Converted To Right-hand-side.
is_lit_atom(?IN) is det: If Is A Literal Atom.
third_order(?VALUE1) is det: Third Order.
boxRule(?KB, ?BOX, ?BOX) is det: Datalog Rule.
diaRule(?KB, ?A, ?B) is det: Dia Rule.
cirRule(?KB, ?A, ?B) is det: Cir Rule.
corrected_modal_recurse(?VALUE1, ?Var, ?OUT) is det: Corrected Modal Recurse.
corrected_modal_recurse0(?VALUE1, ?Var, ?OUT) is det: Corrected Modal Recurse Primary Helper.
corrected_modal(?KB, ?IN, ?OUTM) is det: Corrected Modal.
corrected_modal0(?VALUE1, ?Var, :TermARG3) is det: Corrected Modal Primary Helper.
share_scopes(?KB, ?BDT) is det: Share Scopes.
until_op(?VALUE1) is det: Until Oper..
ct_op(?VALUE1) is det: Ct Oper..
neg_op(?VALUE1) is det: Negated Oper..
b_d_p(?VALUE1, ?VALUE2) is det: Backtackable (debug) Pred.
cnf(?KB, ?A, ?B) is det: Confunctive Normal Form.
cnf1(?KB, ?AS_IS, ?AS_IS) is det: Confunctive Normal Form Secondary Helper.
nonvar_unify(?NONVAR, ?UNIFY) is det: Nonvar Unify.
dnf(?KB, ?A, ?B) is det: Disjunctive Normal Form.
dnf1(?KB, ?DNF, ?DNF) is det: Disjunctive Normal Form Secondary Helper.
simplify_cheap(:TermIN, ?IN) is det: Simplify Cheap.
simplify_cheap_must(?IN, ?IN) is det: Simplify Cheap Must Be Successfull.
pfn4(?KB, ?F, ?PNF) is det: Pnf.
pfn4(?A, ?B, ?C, ?D) is det: Pnf.
cf(?Why, ?KB, ?Original, ?PNF, ?CLAUSESET) is det: Convert to Clausal Form
invert_modal(+KB, +A, -B) is det: Invert Modal.
removeQ(?KB, ?F, ?HH) is det: Remove Q.
removeQ_LC(?KB, ?MID, ?FreeV, ?OUT) is det: Remove Q Lc.
removeQ(?VALUE1, :TermVar, ?VALUE3, :TermVar) is det: Remove Q.
nowrap_one(?Wrap, ?MORE, ?OUT) is det: Nowrap One.
demodal_sents(?KB, ?I, ?O) is det: Demodal Sentences.
to_modal1(?KB, :TermIn, ?Prolog) is det: Demodal.
is_sent_op_modality(?VALUE1) is det: If Is A Sentence Oper. Modality.
atom_compat(?F, ?HF, ?HHF) is det: Atom Compat.
modal2sent(:TermVar, :TermVar) is det: Modal2sent.
clausify(?KB, ?P, ?C, ?C) is det: Clausify.
inclause(?KB, ?P, ?A1, ?A, ?B, ?B) is det: Inclause.
notin(?X, ?Y) is det: Notin.
putin(?X, :TermARG2, :TermX) is det: Putin.
simplify_atom(?H, ?SH) is det: Simplify Atom.
to_regular_cl(?KB, ?H1, ?Has, ?H1) is det: Converted To Regular Clause.
expand_cl(?KB, :TermARG2, ?VALUE3) is det: Expand Clause.
make_clause_set(?Extras, :TermARG2, ?VALUE3) is det: Make Clause SET.
make_clauses(?Extras, ?CJ, ?OOut) is det: Make Clauses.
negate_one_maybe(?Extras, ?One, ?Z) is det: Negate One Maybe.
make_clause_from_set(?Extras, ?Conj, ?Out) is det: Make Clause Converted From SET.
make_each(?Extras, ?Conj, ?E) is det: Make Each.
make_1_cl(?Extras, ?One, ?Conj, :TermOne) is det: make Secondary Helper Clause.
flattenConjs(?Extras, ?I, ?O) is det: Flatten Conjs.
logical_neg(?KB, ?Wff, ?WffO) is det: Logical Negated.
logical_pos(?KB, ?Wff, ?WffO) is det: Logical Pos.
negate_one(?KB, ?Wff, ?WffO) is det: Negate One.
negate(?KB, ?X, ?Z) is det: Negate.
negate0(?VALUE1, ?X, ?X) is det: Negate Primary Helper.
mpred_quf(?In, ?Out) is det: Managed Predicate Quf.
mpred_quf_0(?InOut, ?InOut) is det: Managed Predicate quf Primary Helper.
nonegate(?KB, ?IO, ?IO) is det: Nonegate.
unbuiltin_negate(?Z, ?VALUE2, ?Fml, ?Fml) is det: Unbuiltin Negate.
unbuiltin_negate(?KB, ?Fml, ?Out) is det: Unbuiltin Negate.
removes_literal(:TermX, :TermX) is det: Removes Literal.
delete_sublits(?H0, ?B, ?HH) is det: Delete Sublits.
flatten_clauses(?H, ?HHTT) is det: Flatten Clauses.
correct_cls(?KB, ?H, ?HH) is det: Correct Clauses.
correct_cls0(?KB, :TermCL0, ?CL1) is det: Correct Clauses Primary Helper.
incorrect_cl(:TermH, ?H) is det: Incorrect Clause.
correct_boxlog(?CLAUSES, ?KB, ?Why, ?FlattenedO) is det: Correct Datalog.
correct_boxlog_0(?BOXLOG, ?KB, ?Why, ?FlattenedS) is det: correct Datalog Primary Helper.
variants_are_equal(?Order, ?A, ?B) is det: Variants Are Equal.
cf_to_flattened_clauses(?KB, ?Why, ?NCFsI, ?FlattenedO) is det: Cf Converted To Flattened Clauses.
cf_to_flattened_clauses_0(?KB, ?Why, ?NCFsI, ?FlattenedO) is det: cf Converted To flattened clauses Primary Helper.

Undocumented predicates

The following predicates are exported, but not or incorrectly documented.

clean_repeats_d(Arg1, Arg2)
nnf_args(Arg1, Arg2, Arg3, Arg4, Arg5, Arg6, Arg7, Arg8)
must_map_preds(Arg1, Arg2, Arg3)
sumo_to_pdkb_p5(Arg1, Arg2)
sumo_to_pdkb(Arg1, Arg2)