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

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.


[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


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


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
 pfn4(?A, ?B, ?C, ?D) is det
 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
 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
 clausify(?KB, ?P, ?C, ?C) is det
 inclause(?KB, ?P, ?A1, ?A, ?B, ?B) is det
 notin(?X, ?Y) is det
 putin(?X, :TermARG2, :TermX) is det
 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
 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
 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)