Given a disjunction of conjunctions of the form: A or B or ... or J or K where each capital letter is a conjunction of the form m & n & ... & p & q and each conjunct of the conjunction is of the form m(x, y, ... z, w) where m is a predicate and each term is either a constant or an unbound variable and (elsewhere in the database) there may be several grounded instances of m of the form m(S, T ... V, W) which may unify with the predicates in the disjunction. The objective is to determine if the disjunction is true by determining if one of the disjuncts is true by determining if there exists a case of all of the conjuncts of one of the disjuncts being true through a consistent unification (binding) of the unbound variables in the conjunction with the grounded instances. Also, note that any predicate may be expandable (unfolded) by replacing the predicate with its definition which is of the form: m(x, y, ... z, w) <-> D where D is once again a disjunction as defined above. The following properties would be desirable: 1) Do not waste time recursively following a blind path which possibly has no solution. 2) Do not recompute values. 3) Efficiently determine if their are grounded cases. I am leaning towards the following solution, as of yet unproven, and unimplemented: Within each conjunct, store the links to its neighboring conjuncts which can be linked by common variables. Attempt to find grounded instances of these predicates which can link these conjuncts together. If a pair of conjuncts can be linked, then there is no need to unfold the predicate. If all links within a conjunction can be linked, then the conjunction is proven true. For all links in a conjunct which cannot be linked, unfold one of the predicates and once again attempt to join all the links. Anyone care to explore this problem? Edited by - bishop_pass on June 3, 2001 3:58:21 AM

C''mon people! Here''s a real semi-tough problem for a change with important implications and applications. Let''s see how good you really are.

Can you give us a simple example of a database and what is the program supposed to do (and what is supposed not to do) ?

If you solve this problem efficiently, you have essentially created a process which does all of the following:

1) Proves theorems; that is to say: given an axiom (a rule) it can determine if this rule is inconsistent with the existing database.

2) Finds all axioms which are implied in the database: If the database constains facts P and the rule P->Q and the rule Q->R then it can be determined that R is known.

3) Planning by creating a sequence of steps which satisfies a goal. If the goal is: HypotheticallyTrue(X, T1) & T1 > T where T1 and T represent time, then the T1 will be bound to a functional argument of the form:
do(A, do(B, do (C, do (D, do (E, T))))) where T is the time to start and the sequence of steps to execute are:
E then D then C then B then A.

4) Explanation: given an observation about the environment, through abduction which is a by-product of the algorithm, an explanation is offered for the observations.

5) Truth maintenance for acquisition of new knowledge: if told new rules or facts, assuming these new rules or facts do not conflict with the existing database and all of its implications, the new rules or facts can be assimilated into the database.

6) Disjunctive logic: facts may be vague and imprecise. Not only can reasoning be performed on facts such as A, but also on facts less explicit like A or B, which means the database knows one or the other is true, but doesn't know which one. For example, if the database knows:
A or B
D-> NOT A
D
and if queried to determine if B is true, then the database can reply yes, B is true.



Edited by - bishop_pass on June 12, 2001 11:21:57 PM

How does this apply to game programming?



Dire Wolf
www.digitalfiends.com

quote:

---

Original post by Dire.Wolf

How does this apply to game programming?

---

What if it didn''t? Not everything here has to apply to game programming. But in fact, this has huge applications to game programming. If you want to program Pong, then yes, this algortihm isn''t for you.

But if you want to create games with agents that reason and plan and communicate with each other and can accept or reject that which is communicated to them, then this is for you. If you want agents which observe and acquire knowledge from their environment in a game, then this algorithm is for you. If you want an AI game manager which can store sparse and arbitrary information, then this algorithm is for you. If you want agents which combine reacitve and rational behavior in your games, then this algortihm is for you. If you want a programming environment to create rational AI behavior that is logically consistent with all that the AI knows, then this algorithm is for you. If you want the full expresiveness derived from First Order Logic for what the agents in your game can know, then this algorithm is for you. If you want to get away from canned behavior implicit in scripts and want agents which are constantly assimilating new incoming knowledge, then this algorithm is for you. If you want a system which dynamically generates its own behavior in the form of plans and agendas this algorithm is for you. If you want a system that enables agents to maintain uncertain and incomplete information about their world, then this system is for you. If you would like your agents to maintain not only thier beliefs but beliefs about what other agents believe, then this algorithm is for you. If you want a system that is completely programmable and puts no constraints on the predicates which are available to you, unlike structs which are predefined and are either not totally used or not adequately expressive, then this system is for you. If you would like this system to be as simple and small as your needs require, or as large as your needs require, then this concept is for you.

quote:

---

Original post by bishop_pass

C''mon people! Here''s a real semi-tough problem for a change with important implications and applications. Let''s see how good you really are.

---

Wow, that''s quite a challenge. This is certainly more than semi-tough. You could probably get a PhD thesis out of this.

I''m not going to pretend I have a chance of being a productive help on this one, but I can steer you towards soms papers and a professor I did a short research stint with. He has been working with planners (#3 on your second list) for quite a while. Here''s his webpage: http://www.cs.wright.edu/~mcox/. How did you come up with this idea? There''s some hefty AI problems in there.

Keep me updated...
-Rob

Thanks for the answer, I look forward to your implemented solution.

quote:

---

C''mon people! Here''s a real semi-tough problem for a change with important implications and applications. Let''s see how good you really are.

---

Actually, many of the questions here are real and more applicable to application development than this one (not necessarily game development either). By the way, what textbook did you pull this from?

Out of curiousity, what is your field of expertise in the computer industry?

Best regards,



Dire Wolf
www.digitalfiends.com

Dire.Wolf and rgillen:

The above description of my proposed solution is a rearrangment of a common problem called theorem proving. After reading about Kowalski's IFF procedure, I realized it has a lot going for it, but I wanted to explore the concept of simultaneous AND variable matching instead of his method of expanding equality axioms. Kowalski's IFF procedure, combined with abduction, and built as a reactive and rational agent, has almost all of the traits I listed above, except for full theorem proving.

Also motivated by Stickel's PTTP (Prolog Technology Theorem Prover), one of the faster theorem provers out there, I got the idea that the concept behind it could be faster if it didn't blindly search one of the conjuncts with SLD resolution without first making sure there is a unifiable solution joining all of the current unfolded conjuncts.

Standard theorem proving uses resolution, which explodes the problem unnecessarily, and makes the search space much bigger than it needs to be.

I have no profession in the computer industry, just lots of years of reading and researching in my own time. I've already spent a great deal of time studying 3d graphics, so I have moved my interests into AI.

I have figured out a solution based on what I call sequences and efficient lookup via hash tables. I need to set down and write the code. I still have no idea whether it will work fast enough on hard problems or large databases, but I think it has something going for it that the other solutions don't, and that's preventing the search space from growing until it's clear that a solution cannot be derived from the current expansion of the problem.

As far as the byproducts of the solution, that is just standard theorem proving, event calculus, and abduction as defined in the literature. It's how it finds the solution that makes the difference.

Here's a simple example that isn't using functional aguments. Look at the axiom below which says: if A is the ancestor of B and B is the ancestor of C, then A is the ancestor of C.

Ancestor(x,y) <- Ancestor(x,z) & Ancestor(z,y)

This is First Order Logic and can also make statements about existential knowledge and disjunctions. If you convert the above statement to normal form, you get:

~Ancestor(x,z) | ~Ancestor(z,y) | Ancestor(x,y)

The '~' means NOT. The resoltiuon process uses the normal form. If instead you leave it in definitional form, then you rearrange the terms in such a way that the conditional side (in this case the right hand side) is made to be a disjunction of conjunctions.

So, we have it in it's original form, which is:

Ancestor(x,y) <- Ancestor(x,z) & Ancestor(z,y)

Now, there would be other definitions also, such as ones about parents and age and mothers and siblings, but for simplicity, let's leave these out. Suppose we have the following grounded literals: (these are facts)

Ancestor(Bob,Bill)
Ancestor(Bob,Jack)
Ancestor(Bob,Mary)

Ancestor(Mary,Fred)
Ancestor(Mary,Rich)

Ancestor(Rich,Joe)

If we look at this, we can see that Ancestor(Bob,Joe) is a true, but implicit fact. To fully understand the problem, visualize a tree where each node is a person, and all children of the node are children of that person. Additionally, visualize that each node has not just one parent, but two. So we have a tree expanding in both directions. Now, take any random node and another random node, and see if they are linked via an Ancestor relation. The main problem is you don't know how deep the tree goes on any given branch, so it is NOT a good strategy to explore one branch all the way in hopes that branch leads you to the other node. Therefore, we want to explore all branches simultaneously, seeing if there is any solution along the way.

Here's how it works:

Query:
Ancestor(Bob,Joe)?

We hash into a table and instantly discover if the grounded literal Ancestor(Bob,Joe) exists. It does not. So, according to the definition of Ancestor, it is unfolded and we get the following:

Ancestor(Bob,y) & Ancestor(y,Joe)

Compiled with this axiom is a set of sequences, which is a table defining a procedure of how each conjunct is dependent on the other. We hash into the table with Ancestor(Bob,*) and instantly get (because of the way the table is organized) a list of all the possible bindings for y. The sequence table says: take the first binding for y and test it with the 2nd conjunct. In this case, we see if there is the grounded literal:

Ancestor(Bill,Joe)

That fails, so the sequence table says go back and try the next. So we try

Ancestor(Jack,Joe)
Ancestor(Mary,Joe)

These both fail, so we unfold one of the predicates, and we have the new sequences:

Ancestor(Bob,y) & Ancestor(y,z) & Ancestor(z,Joe)

This does have a solution and it will be found by testing it's sequences without anymore recursive exploration of the search space. Also, note that as the sequences move from left to right, the variables gain bindings and become more restrictive in what they allow to introduce into the search space.

Edited by - bishop_pass on June 4, 2001 1:24:55 PM

It''s worth noting that the above process of attempting to prove a query occurs in lockstep with a process attempting to prove the negation of the query. So, in reality, we have the two procedures attempting proofs at the same time:

1) Ancestor(Bob,Joe)
2) ~Ancestor(Bob,Joe)

So, if query 1 returns a solution first, then the answer is TRUE and no forther processing is necessary. If query 2 returns a solution first, then the answer is FALSE, and no further processing is necessary.

To prove negations, negative axioms are required. In many instances, negative axioms are derived from the positive axioms. In the case of Ancestor, an explicit negative axiom would be like the following:

~Ancestor(x,y) <- Ancestor(y,x)