Package "logicmoo_base"

Title:	LogicMOO - Extends Prolog Programming to support Dynamic Epistemic Logic (DEL) with Constraints
Rating:	Not rated. Create the first rating!
Latest version:	2.0.3
SHA1 sum:	724b8d33393185634281ccc938fdcc4c647f39ee
Author:	Douglas R. Miles <logicmoo@gmail.com>
Home page:	https://github.com/TeamSPoon/logicmoo_base/
Download URL:	https://github.com/TeamSPoon/logicmoo_base.git/release/*.tgz
Requires:	instant_prolog_docs
	logicmoo_utils
	multimodal_dcg
	pfc
	wam_common_lisp

Reviews

No reviews. Create the first review!.

Details by download location

Version	SHA1	#Downloads	URL
2.0.3	5d224682e6983132644f9b641eea63a83aeb298c	1	https://github.com/TeamSPoon/logicmoo_base.git
	53fdc543967895568f8357c6cdabc1df8affb9b3	1	https://github.com/TeamSPoon/logicmoo_base.git
	0e2b43bdaae082f9a5f66bdecda73a9488060591	3	https://github.com/TeamSPoon/logicmoo_base.git
	724b8d33393185634281ccc938fdcc4c647f39ee	3	https://github.com/TeamSPoon/logicmoo_base.git
	16518b4135f0822d743c5eb35149fdc218b76566	5	https://github.com/TeamSPoon/logicmoo_base.git
	679789ecda03c586f02f642b38e614a2f925720d	13	https://github.com/TeamSPoon/logicmoo_base.git
1.4.111	90f365d7c072a2c33e27f44ef22010c895f89647	1	https://github.com/TeamSPoon/logicmoo_base.git
	701ed64cb5605505dea488deb4c4319faac83ad5	4	https://github.com/TeamSPoon/logicmoo_base.git
	632aed8804c31d5d568fba643b67c960208e8d94	1	https://github.com/TeamSPoon/logicmoo_base.git
	c270810132cff93efb754e62cdadf8e7caa4e663	1	https://github.com/TeamSPoon/logicmoo_base.git
	160193e8aa3f94fdcf50f36234c2ebddceaa05e5	1	https://github.com/TeamSPoon/logicmoo_base.git
1.3.111	a67425df0879f01e39bd83f4db5526712a7dfc4c	2	https://github.com/TeamSPoon/logicmoo_base.git
	f12aa34457734c9cc2981bf9bbf2b9bb9a5e1472	5	https://github.com/TeamSPoon/logicmoo_base.git
1.2.111	2da8df4bdf4f0e5a2dd14fb8533cb54dc497ae7f	2	https://github.com/TeamSPoon/logicmoo_base.git
	7ca6ad43c899dba3227717126cf0173f7e4e6a54	7	https://github.com/TeamSPoon/logicmoo_base.git
1.1.118	1635841679802612dd5195beceeb9a06b01f0067	1	https://github.com/TeamSPoon/logicmoo_base.git
	409b9b5bba1d82f98c165d234d42c394c4921bb4	1	https://github.com/TeamSPoon/logicmoo_base.git
	29a5cc04cc6aad1d57f50b12ce4af50e2bf1eed5	1	https://github.com/TeamSPoon/logicmoo_base.git
	9c64dac12f872ea9365a17f07ed99518fa49c806	1	https://github.com/TeamSPoon/logicmoo_base.git
	4e8909132bacd8052cd0d4e3ea68e5f46f37e2f8	1	https://github.com/TeamSPoon/logicmoo_base.git
	fab851f3a6e1e9f22c547d041dbd3d8616c66ff3	1	https://github.com/TeamSPoon/logicmoo_base.git
	dcccd979fa8baafe4613b608bd3983246bec19dc	1	https://github.com/TeamSPoon/logicmoo_base.git
	6b75b7abfc48822ce0767a3466cbed3748c8fa72	1	https://github.com/TeamSPoon/logicmoo_base.git
	396ed2fc19c88760264ba7f9bda88ca7a50b47a6	1	https://github.com/TeamSPoon/logicmoo_base.git
	d7e0385290c41cf64cf48f04fe0e9d6cb80c4f35	1	https://github.com/TeamSPoon/logicmoo_base.git
	651e7b0a7260f0be85a2cbe58ffe9532d6e50575	1	https://github.com/TeamSPoon/logicmoo_base.git
	09f4f3e343bf6dcf616afe857b05e4bbd925654b	1	https://github.com/TeamSPoon/logicmoo_base.git
	990e041c963a23e1dd7ce4ed2cfafa9afc20a52f	2	https://github.com/TeamSPoon/logicmoo_base.git
1.1.117	cb66ee57c356ea74c08a1fb43a0712eafb1446c3	1	https://github.com/TeamSPoon/logicmoo_base.git
1.1.115	afa918e23b3d65254010491b65d48e3ed3c6ca33	1	https://github.com/TeamSPoon/logicmoo_base.git
1.1.112	78c789b6107e10d5c9b40f18fd23f2baa13bdde8	1	https://github.com/TeamSPoon/logicmoo_base.git
1.1.1	f599efdb9b3f05cdbdac89ef02f76bcf013e90dd	5	http://www.prologmoo.com/packs/logicmoo_base/release/logicmoo_base-1.1.1.tgz
1.0.1	35874d6d653711c4145b4998ce21b84fd6370be3	1	http://www.prologmoo.com/packs/logicmoo_base/release/logicmoo_base-1.0.1.tgz
0.0.16	c07b5023e4ba970db8b586d1ed8bc19358b4f90b	1	http://www.prologmoo.com/packs/logicmoo_base/release/logicmoo_base-0.0.16.tgz
0.0.15	a26a41cdb2aedc931e3b4cb018c734889df7f7df	1	http://www.prologmoo.com/packs/logicmoo_base/release/logicmoo_base-0.0.15.tgz
0.0.14	584b50132e034e96bbd17652fb005626cb440e12	1	http://www.prologmoo.com/packs/logicmoo_base/release/logicmoo_base-0.0.14.tgz
0.0.13	3d0a5f2a57e1c30c107727286479920a522f4523	1	http://www.prologmoo.com/packs/logicmoo_base/release/logicmoo_base-0.0.13.tgz
0.0.12	dd6e93fb796ea7fb5e119a4b2cc4ba4479bfdc5f	1	http://www.prologmoo.com/packs/logicmoo_base/release/logicmoo_base-0.0.12.tgz
0.0.11	b012c04951a87a17eec766e8ee7769ca9709d149	1	http://www.prologmoo.com/packs/logicmoo_base/release/logicmoo_base-0.0.11.tgz
0.0.10	648da1a81cc5c68726990f22ff7e9c7456ecf2de	1	http://www.prologmoo.com/packs/logicmoo_base/release/logicmoo_base-0.0.10.tgz
0.0.9	9785bf98b04f1b9aed85bd58b2af919a797f6fc7	1	http://www.prologmoo.com/packs/logicmoo_base/release/logicmoo_base-0.0.9.tgz
0.0.8	8dff5e3d2dec404472c2c5c1811ebf55881ce167	1	http://www.prologmoo.com/packs/logicmoo_base/release/logicmoo_base-0.0.8.tgz
0.0.7	5da7714001ed25b01369407159c56843d4622ffc	1	http://www.prologmoo.com/packs/logicmoo_base/release/logicmoo_base-0.0.7.tgz
0.0.6	efeb58a127cf2fa4454a32a8ed78ff9d89803ef5	1	http://www.prologmoo.com/packs/logicmoo_base/release/logicmoo_base-0.0.6.tgz
0.0.5	b6942f3dd1cec7b82afbebae3508e16b03dcd597	3	http://www.prologmoo.com/packs/logicmoo_base/release/logicmoo_base-0.0.5.tgz
0.0.4	7cb406c3947a88351d5228be5b5d7f36e89c830a	1	http://www.prologmoo.com/packs/logicmoo_base/release/logicmoo_base-0.0.4.tgz
0.0.3	d2dd7c76a86f49e40c93f4c722427aecfbde1d6f	1	http://www.prologmoo.com/packs/logicmoo_base/release/logicmoo_base-0.0.3.tgz
0.0.2	7be944661f62576d10f6c2272e6f5974f38f5e79	1	http://www.prologmoo.com/packs/logicmoo_base/release/logicmoo_base-0.0.2.tgz
0.0.1	b38820f0b4508998d1ed06584293453fff66238b	1	http://www.prologmoo.com/packs/logicmoo_base/release/logicmoo_base-0.0.1.tgz

logicmoo_base

Knowledge Base Maintenance System

?- ensure_loaded(library(logicmoo/logicmoo_base)).

:- file_begin(pfc).
spouse(X,Y) ==> spouse(Y,X).
gender(P,male) <==> male(P).
gender(P,female) <==> female(P).

Defining new General Inference rules

?- ensure_loaded(library(logicmoo/logicmoo_user)).

:- file_begin(kif).

parent(X,Y),female(X) <=> mother(X,Y).
parent(X,Y),parent(Y,Z) => grandparent(X,Z).
grandparent(X,Y),male(X) <=> grandfather(X,Y).
grandparent(X,Y),female(X) <=> grandmother(X,Y).
mother(Ma,Kid),parent(Kid,GrandKid)
      =>grandmother(Ma,GrandKid).
grandparent(X,Y),female(X) <=> grandmother(X,Y).
parent(X,Y),male(X) <=> father(X,Y).
mother(Ma,X),mother(Ma,Y),{X\==Y}
     =>sibling(X,Y).

examples: https://github.com/TeamSPoon/PrologMUD/tree/master/pack/logicmoo_base/t/examples/fol

First Order Logic (FOL) declarations in Prolog source code.

Despite Prolog's logic heritage it does not qualify as a full general-purpose theorem-proving system. There are three main reasons: (1) Prolog is a programming language and not an inference engine so if we used the unification algorithm of Prolog for FOL, it is unsound, (2) Prolog's unbounded depth-first search strategy is inefficient when it is doing complete search, and (3) Prolog's inference system is not complete for non-Horn clauses. Nevertheless, Prolog is quite interesting from a theorem-proving standpoint because of its very high inference rate as compared to conventional theorem-proving programs.

Logicmoo use of the Prolog Technology Theorem Prover (PTTP) was to overcome the deficiencies while retaining as fully as possible the high performance of well-engineered Prolog systems.

The Prolog Technology Theorem Prover (PTTP) is an extension of Prolog that is complete for the full first order predicate calculus (Stickel, 1988). It is invoked whenever the facts and rule are described in NNF or CNF put into the knowledge base. And optionally for Horn clauses built by other modules. However, when the rules are in Prenix Normal Form (PNF) (thus have quantifiers) they are converted to NNF, SNF and finally CNF and handed back over to PTTP. Also a formula whose leading quantifier is existential, the formula obtained by removing that quantifier via Closed Skolemization may be generated.

kif_add/1: the file has a rule or fact, in the form of a predicate of FOPC (First Order Predicate Calculus). The LogicMOO invokes the PTTP compiler (discussed later) to assert the form to the knowledge base. The knowledge base represents the user''s beliefs. Thus, asserting the logical form to the knowledge base amounts to applying the Declarative rule and the Distributivity rule (Axiom B2).

kif_ask/1: the user types in a question, in the form of a predicate of FOPC (First Order Predicate Calculus). The PTTP inference system is then invoked to attempt to prove the predicate, using the axioms and facts of the knowledge base. This amounts toassuming that the user''s beliefs are closed under logical consequence, i.e., the Closure rule (Axiom B1) is implicitly applied over and over.

LogicMOO, because of PTTP, is unlike all other theorem provers today (Perhaps except SNARK and maybe CYC) Here is how:: If the proof succeeds, LogicMOO answers yes'', and prints out the predicate, instantiating all variables. If there are multiple answers, then it prints all of them. If the proof fails, LogicMOO invokes PTTP to prove the negation of the queried predicate. If that NEGATED proof succeeds, then LogicMOO answers no''; otherwise, LogicMOO answers ``cannot tell, not enough information''.

LogicMOO, therefore, has the capability for reasoning about negation, being able to distinguish between real negation (P is false'') from negation by failure (P is not provable''). This allows the system to distinguish beliefs that are provably false from beliefs that cannot be proven because of insufficient information. This is an important feature that overcomes the supposed limitations of Prolog. For example, without this added capability, if a user were to ask whether LogicMOO believes that John intended to let the cat out, then LogicMOO would answer no''. This answer is misleading because LogicMOO would also answer no'' if it were asked if John did not intend to let the cat out. This is why the system automaically Re-asks the negation.

Sadly all theorem provers since PTTP (include theorem provers said to be based on it) have been simplified to to no longer do this simple analysis. The reason? According to classically trained logicians horn clauses cannot start with a negated literals. So to not offend them (entirely) PTTP can store "( ~a :- ~b )" as "( not_a :- not_b )" If we obeyed the classical limitations set forth upon Horn clauses to only being "positive" that would remove the unique ability for LogicMOO to deduce the difference between false and unknown. We are no longer restricted to CWA and the limitations imposed by modern theorem provers and sematic web tools. I must assume the reason programmers made these sacrifices is they can still solve problems like circuit verifcation without disrupting the post 1980s maintsteam thinking.

Since LogicMOO can infer the limits it's theoretical knowledge, so it can help guide the user to understand what types of knowledge it is missing. That also provides a portal through which other modules (e.g., a plan recognition system or a modules for NL reference resolution) can enter information. When such modules are not available, the user may simulate this capacity. ("ask the user")

is_entailed_u/1: Detects if an Horn Clause (or fact) is holograpically existing. Example: assert a=>b. this will result in the following two clauses: is_entailed_u(( ~a :- ~b )) and is_entailed_u(( b :- a ) ).

Backward-Chaining Rules

PFC

Pfc includes a special kind of backward chaining rule which is used to generate all possible solutions to a goal that is sought in the process of forward chaining.

Forward chaining macros

It is well known that sound and complete reasoning systems can be built using either exclusive backward chaining or exclusive forward chaining. Thus, this is not a theoretical problem. It is also well understood how to ``implement'' forward reasoning using an exclusively backward chaining system and vice versa. Thus, this need not be a practical problem. In fact, many of the logic-based languages developed for AI applications allow one to build systems with both forward and backward chaining rules. There are, however, some interesting and important issues which need to be addresses in order to provide the Prolog programmer with a practical, efficient, and well integrated facility for forward chaining.

This module uses such a facility, written by Tim Finin called PFC, which he has implemented in standard Prolog. The PFC system is a package that provides a forward reasoning capability to be used together with conventional Prolog programs. The PFC inference rules are Prolog terms which are asserted as facts into the regular Prolog database.

The PFC system package provides a forward reasoning capability to be used together with conventional Prolog programs. The PFC inference rules are Prolog terms which are asserted as clauses into the regular Prolog database. When new facts or forward reasoning rules are added to the Prolog database (via a special predicate pfc_add/1, forward reasoning is triggered and additional facts that can be deduced via the application of the forward chaining rules are also added to the database. A simple justification-based truth-maintenance system is provided as well as simple predicates to explore the resulting proof trees. Additionally this module provides the user with various methods for trying out new techniques of backwards chaining without rewriting their code.

The logicmoo_base module allows one to use optimal First Order Logic declarations in Prolog code. During development, these declarations log informative information when values don't match expectations. A typical development environment converts this into a helpful stack trace which assists in locating the programing error.

You may have noticed that Logicmoo defines {}/1 as an escape construct for bypassing the FOL's salient body goals.

% this means that both P and Q can't be true.
disjoint(P,Q), {current_predciate(_,P),current_predciate(_,Q)}
  ==>
  (P ==> not(Q)),
  (Q ==> not(P)).

As exemplified above, this is the same control construct that is used in grammar rules for bypassing the expansion of rule body goals when a rule is converted into a clause. Both control constructs can be combined in order to call a goal from a grammar rule body, while bypassing at the same time the Prolog compiler. Consider the following example:

S-Expr reader utilities

The abiliity to use CLIF/KIF/CycL Etc

Source code available and pull requests accepted on GitHub: https://github.com/TeamSPoon/PrologMUD/tree/master/pack/logicmoo_base

Some TODOs

Document this pack! Write tests Untangle the 'pack' install deps Still in progress (Moving predicates over here from logicmoo_base)

BSD 2-Clause License

Copyright (c) 2017, Douglas Miles <logicmoo@gmail.com> and TeamSPoon All rights reserved.

Not obligated to maintain a git fork just to contribute

Dislike having tons of forks that are several commits behind the main git repo?

Be old school - Please ask to be added to TeamSPoon and Contribute directly ! Still, we wont stop you from doing it the Fork+PullRequest method

Contents of pack "logicmoo_base"

Pack contains 1,117 files holding a total of 24.7M bytes.