Did you know ... Search Documentation:
 Pack logicmoo_base -- prolog/logicmoo/common_logic/common_logic_compiler.pl

Provides a prolog database replacement that uses an interpretation of KIF

t/N hybridRule/2

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.

Copyright (C) 1999 Anthony A. Aaby <aabyan@wwc.edu> Copyright (C) 2006-2007 Stasinos Konstantopoulos <stasinos@users.sourceforge.net> 1999-2015 Douglas R. Miles <logicmoo@gmail.com>

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:

TBE ::= BEXPR | final TBE ::= `always(TBE)` | `eventually(TBE)` | `until(TBE,TBE)` | `release(CT,TBE,TBE)` | `cir(CT,TBE)`
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
clean_repeats_d(?PTTP, ?PTTP) is det
Clean Repeats (debug).
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.

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)