Programming Interactive Worlds with Linear Logic
cs.cmu.edu
cs.cmu.edu
If the author is reading this, please consider submitting your work to some literary theory journals. Literary theory has decayed into something tired and vague, and this sort of heroic formalism could really make a splash! I mean, this is actual literary theory!
I wonder what the relationship is between linear logic and the logic of [2].
[1] http://versu.com
edit: the magic of a little bird: http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6...
Linear logic is obtained from a classical logic in which entailment is not monotonic or idempotent. That is, a statement X && Y && Y proves Z cannot be contracted to X && Y proves Z, nor can the statement X proves Z be weakened to X && Y proves Z. One interpretation of this lets you treat terms as resources which cannot be created out of thin air. This is really useful for modeling logical constraints on resources and their allocation.
Modal logics on the other hand are a very wide family of logic systems (see [0] for a diagram of some of the most simple modal logics) which introduce new operators to encode modality, a kind of qualification of the truth of a statement. For example a modal operator might encode that a statement is prohibited, that its truth is unknown, or that a statement will be true at some point in the future. These modal operators make modal logics useful for describing temporal constraints, or encoding logical statements about the belief of agents in a system (imagine giving each agent a modal operator B_i(X) which means, agent i believes X). In the latter case, different agents can hold incompatible beliefs without creating contradiction.
As I understand it, Evans' cathoristic logic (the name of which the paper claims has greek origins, meaning "to impose narrow boundaries") arises from the desire to simply express inferences between atomic sentences with the expressivity of natural language. First-order logic is able to encode many natural language statements, such as adverbials, inference from dyadic to monadic propositions, and handling incompatible statements. However, first-order logic requires us to introduce quantifiers to do so, vastly increasing the search space for decision and resolution of these propositions.
To get around the problem of quantifiers without losing expressivity, cathoristic logic uses subset of Hennessey-Milner logic[1] as a starting point. Negation is excluded, as it is the weakest form of encoding incompatibilities. For instance, in first-order logic, asserting "Pierre is the only king of Spain" is the same as saying "For all individuals other than Pierre, that individual is not the king of Spain". This weakness requires the knowledge-representer to include an axiom for every excluded possibility, or generalize the statement with a quantifier so that it no longer becomes atomic. Evans' therefore introduces the Tantum operator (written !A, for some set A) to express that the members of A exhaust all possibilities (almost like the latin abbreviation viz). Using the Tantum operator, we can reformulate the example above to be: "The king of spain is (Pierre && !{Pierre})".
Using this operator lets one make specific optimizations when running the decision algorithm, and the paper shows that it's able to perform decisions in quadratic time. If negation were included, the running time for decision would be superpolynomial.
Thanks for sharing the paper and prompting my read-through of it!
[0]: http://plato.stanford.edu/entries/logic-modal/#MapRelBetModL...
[1]: https://en.wikipedia.org/wiki/Hennessy%E2%80%93Milner_logic
classic:
if $5 then pizza
if $5 then beer
$5!
therefor: pizza AND beer
if $5 then pizza
if $5 then beer
$5!
therefor: pizza OR beer
if $5 then pizza
if $2 then beer
$6!
In the example you gave:
if $5 then pizza
if $2 then beer
$6!
therefore, (pizza and $1) OR (beer and $4) OR (beer and beer and $2) OR (beer and beer and beer) OR $6The Ceptre tutorial even has the classic example of moving blocks on a table. It's a different language than STRIPS (using PDDL), but seems a similar idea.