An idea that Namaste and I had for the linguistic magic system was to have the spells that are cast alter the laws of the universe. Clearly this is a hard problem. But I like hard problems (see, for example, Minesweeper Infinity and Flamethrowerflies :-p). My current plan is to lay out a grid where each space may have any number of several properties. These properties interact with the players in predefined ways, but the way that they interact with each other will be defined by the user during the game.
Let’s say that two of these properties are fire(p,t) and water(p,t) (where p is position and t is time) One of the rules that a sorcerer could define would be: forall p t. !(fire(p,t) and water(p,t)), i.e. fire and water cannot be at the same place at the same time. Then the rendering phase would iterate over each position in the world and ask whether fire(p,t) is true, and if so, draw some fire there, and do the same for water.
This requires a logic engine almost, but not quite, entirely unlike Prolog. This logic engine must have the following property: if a formula’s truth value can be derived in a finite amount of time, then the engine must derive it in a finite amount of time (crossing my fingers that the construction of such an algorithm is even possible). Prolog most certainly does not have this property. Doing this for any logical form would be ideal, but I am okay with restricting the types of formulas that can be constructed. For example, universal quantification may be disallowed in queries and rules must be universal implication (the rule “fire exists” would be disallowed).
Thanks to Gödel, we know that there will either be a formula that can be proven both true and false or a formula which cannot be proven either. If fire(p,t) happens to be one of these formulas, I’m not sure what to do. We can’t just let the engine diverge (infinite loop).
The first step in my process would usually be to define a normal form that the formulae take. For example, Prolog defines rules as Horn clauses. However, when you ask Prolog a question, it either returns “yes this is true” (and gives you assignments to your variables) or “I cannot prove this”. My engine must return “yes this is true”, “no this is not true”, or “I cannot prove this either way” (and of course, “I’m still trying to prove this, but I’ve taken too long”). For example, if you have a rule “p(x) ⇒ q(x)”, the engine can either use p(x) to prove q(x) or use not q(x) to prove not p(x). It is not clear that Horn clauses have a property that makes this easy.
Hmm, actually Horn clauses have a property that makes this quite easy. Let’s say you have the formula: ∀x (∃y p(x,y) and q(x,y)) ⇒ r(x). Note that this is a Horn clause. We can apply the contrapositive and do some massaging to obtain the formula: ∀x ∀y ¬r(x) and p(x,y) ⇒ ¬q(x,y). Note that this is also a Horn clause. If there are variables that do not appear in the right side of the implication, they will be existentially quantified on the left, as the Horn clause requires. So basically, you can naively transform the Horn clause A,B⇒C to ¬C,A⇒¬B and also to ¬C,B⇒¬A. You can derive negation rules for every predicate you depend on.
With a breadth-first evaluation strategy (which is necessary for the “derivability” constraint above), you can attempt to derive multiple things at once, and stop at the first one you get to. So to ask for the truth of a statement P, you simply try to derive P and ¬P at the same time. You go with whichever one comes up first, and you cross your fingers and hope that it’s not possible to prove its negation (If it isn’t, then you’ll spin your wheels forever trying to prove it. If it is possible, then you will eventually prove it and show inconsistency. I.e. you can show that you are inconsistent, but you can never show that you are consistent.).