Modal Logic discussion logs

00:43 <meditans> I guess the broad question I have is: what kind of logic should I be familiar with to do something like versu?
00:44 <meditans> e.g. is modal logic actually used in things like this?
00:45 <meditans> or is solving in those sistem too difficult to be useful in practice?
00:46 <•doppioslash> Javier Torres ( @drtowerstein ) is looking into modal, Chris Martens uses linear, Evans used exclusion logic, but what are their characteristics and why should one be chosen over the others? Or maybe they can work together?
00:54 <meditans> so, combining linear logic and modal logic is possible, per se (eg https://encrypted.google.com/url?sa=t&rct=j&q=&esrc=s&source=web&cd=1&cad=rja&uact=8&ved=0ahUKEwisl8rQrarJAhUIaRQKHe_yAO4QFggcMAA&url=http%3A%2F%2Feprints.soton.ac.uk%2F261814%2F1%2Ftphols03.pdf&usg=AFQjCNHzYK2B2fOqWHd7u2lrUlZnIeOlPA&sig2=M7ZsGp2n9TxOBHvZ5uAE5g), the question is: is it useful in this context
00:55 <augur> ok back, lemme look for that video
00:55 <augur> i soooorta use modal logic in LE, but in the next revision im probably going to drop it entirely
00:55 <meditans> what's LE?
00:56 <augur> Language Engine, by AI project / putative startup
00:57 <meditans> oh, yeah, doppioslash linked it yesterday, interesting stuff
00:57 <•doppioslash> what does modal logic provide to it?
00:57 <meditans> and why are you considering dropping it?
00:57 <augur> doppioslash: the way coded up imperativity in the current version of LE is as a kind of modality

00:58 <meditans> what do you mean with "imperativity"
00:58 <meditans> ?
00:58 <augur> commands, basically
00:58 <augur> rather than assertions or questions
00:58 <meditans> could you explain a bit how that is a modality?
00:59 <augur> so like... Imp(A) means roughly "Do A" and a proof of Imp(A) is kind of like an IO action in Haskell, in that it's an instruction for how to actually do A
00:59 <augur> so when the user says "Do A", the system tries to construct a proof of Imp(A) which it then executes
01:00 <augur> in some sense, Imp(A) is a possibility modality, "It's possible to make A true", and a proof of that ought to be exactly a recipe for how to make A true
01:01 <meditans> that makes sense.. so is the proof of Imp(A) an opaque object?
01:01 <augur> i'm dropping it from LE because the bigger picture of how discourse should go seems, imo, to work better without a specific modality like that
01:01 <augur> no, it doesnt have to be an opaque object at all
01:01 <augur> i mean, haskell's IO is opaque b/c of implementation reasons, but you can implement it perfectly well as a first order data type
01:02 <augur> data IO a where  GetStr :: IO String  ;  PutStr :: String -> IO ()  ;  ...
01:02 <meditans> ok, so in the proof of Imp(A), who are the leaves in the derivation tree?
01:02 <augur> its just not so efficient to then ship that to an executor to traverse the command tree
01:03 <augur> either returns or requests for primitive actions that are more or less equivalent to GetStr and PutStr there
01:05 <augur> so in a simplification, consider:   copy the file. the meaning of this might be just   Imp (exists x. Copy f x)    where f is the file in question
01:05 <augur> this is a rough sketch mind you :p
01:06 <augur> to make it true that there's an x that is a copy of f, you need to first make an x (at least at the symbolic/representational level)
01:06 <meditans> yes thanks, I understand that, now I'm trying to understand why this is framed in terms of modality
01:06 <meditans> why don't you just consider it a proposition with a very easy proof?
01:06 <augur> so a proof of Imp (exists x. P) is a gadget that makes an M, and then a proof of Imp [M/x]P
01:07 <augur> well, it's framed in terms of modality because at the time i was thinking of it in terms of modality :)
01:07 <augur> i mean, partly you have to keep in mind that this is dealing with *dynamics*, right
01:07 <augur> if i say "Make a copy of the file" it is not true *right now* that there's a copy of x
01:08 <augur> in fact, we expect it to be _false_ that there's a copy of x, maybe
01:08 <meditans> oh, that makes sense

01:08 <meditans> so this is, broadly speaking, a temporal modality?
01:08 <augur> yeah, so there's something more going on that just what's true in the eternal now
01:08 <augur> yeah its kind of temporal
01:09 <augur> i mean, i was thinking of it as a kind of diamond/possibility modality
01:09 <meditans> thanks, now I got a clearer picture of the process
01:09 <augur> and if you think in terms of a possible worlds semantics, <>P means "at some accessible world, P"  fsvo "accessible", right
01:10 <augur> so if you think of that kind of temporally, there's some way to move to a "next" world/moment/whatever where P is true
01:11 <meditans> and in this particular case the accessibility relation is guided by your primitive operations of creating/moving/ecc, right?
01:11 <augur> so its not mere logical or epistemic possibility, say, but some kind of action possibility that you prove by showing you have a means to do it
01:11 <augur> yeah, the proofs incorporate the primitives
01:11 <augur> tho the accessibility relation is just an intuition, it's not present in anything :)
01:12 <augur> i mean, i suppose it would be present if you gave a denotational semantics for this but that's not very proof-theoretic and im a proof-theory nerd x3
01:12 <augur> also hi saolsen, ebutler!
01:12 <meditans> ok, I got the gist of it; so how can this be done without modality?
01:12 <meditans> I mean, why doesn't this approach convince you anymore?
01:13 <meditans> hi all :)
01:13 <augur> well so the reason i moved beyond a modality is because the means by which humans actually issue commands, or ask questions, etc. is much funnier than just using a particular syntax for imperatives
01:14 <augur> consider "Would you mind copying this file?" which is strictly speaking a question but is clearly intended to actually be a polite command
01:14 <ebutler> hi!
01:15 <•doppioslash> ebutler: hello :)
01:15 <•doppioslash> hi saolsen
01:15 <augur> the gricean approach that im taking is that instead, speech acts can be interpreted in various ways so as to establish the speaker's goals/desires/intentions/whatever  and the computer, being a co-operative and obedient computer, will try to achieve those goals as best as it can
01:17 <augur> so "Would you mind copying this file?" seems like a question, and maybe you want to answer it, but you also are inferring the speaker's goal of actually *getting you* to copy the file, and so you work to achieve that goal, rather than just being a jerk and saying only "no i wouldnt mind"
01:17 <meditans> I see.. at which point of parsing is the logic structure introduced?
01:18 <meditans> or, what is the result of parsing a sentence?
01:18 <augur> oh dont worry about that, it's kind of tangential :)
01:18 <augur> there are all sorts of ways to do it, but you end up with the same thing, so abstract over it
01:19 <meditans> I'm asking because, after having parsed the sentence, don't you still need to deal with the "satisfiability modality" above for executing the command?
01:19 <augur> not really. so the end result of parsing a speech act is something which looks more like just a proposition about an action
01:20 <augur> "Copy the file"   looks more like   "I command you to copy the file"   in some sense
01:20 <augur> and then what you do in response to that **statement** depends.
01:21 <meditans> ok, that's what I meant with "at which point". The logical structure is introduced within parsing, so you have to have a richer framework to accomodate all the possible ways of formulating the request
01:21 <meditans> (correct me if I'm wrong, I'm still wrapping my mind around this xD)
01:21 <augur> by the end of parsing you have a proposition in (a variant of) intuitionistic type theory
01:22 <augur> Command(augur,meditans,Copy(meditans,the_file))
01:22 <meditans> that's very nice :)
01:22 <augur> if you're my underlying, this would create a goal in your mind of making it true that  Copy(meditans,the_file)   or whatever
01:23 <augur> and then you prove that goal in various ways, which end up being actions, sort of
01:23 <meditans> yeah, so I would just prove it
01:23 <augur> but consider also, i could say "I need a copy of this file"
01:23 <augur> and thats not a command, its a statement of fact
01:24 <augur> maybe something like   Need(augur, exists x. Copy(the_file,x) & Have(augur, x))
01:24 <augur> and if you're nice, you might say, how can I make it true that   "exists x ..."??
01:25 <augur> and then by working to prove that, you end up with a subgoal where you copy the file
01:25 <augur> just like before, with the imperative, only now you got that subgoal from an assertion
01:25 <augur> so in this system, its assertions all the way down
01:26 <augur> assertion + participant's cooperation => action
01:26 <meditans> that's very clever, I'd like to know more on where is complexity hiding here, in your opinion
01:27 <meditans> which is the most complex part of the chain going from parsing to executing the action?
01:27 <augur> well. to make this work, you need to have a general way of working back from goals to things that can realize them, so you need all sorts of backward-chaining theorem proving
01:27 <augur> but the real hard part, and which will remain hard for a while, is inferring the speaker's intentions
01:28 <meditans> right, as we're talking about this, why backward chaining? Is this the best method in general?
01:29 <augur> well, probably your knowledge of what you can do is very vast
01:29 <augur> like, not just a few dozen "rules", but probably thousands, or 10s of thousands
01:29 <meditans> eg, I saw there is something called "resolution", but that's applicable only when you have a disjunctive normal form, right?
01:29 <augur> and if you forward chain from nothing, you'll be hosed
01:30 <augur> you need to work back from your goal, so that you cut out most of the search space
01:30 <augur> but thats just a hunch for where to start. im sure some focusing provers would work fine, maybe
01:30 <augur> i dunno
01:31 <augur> im not sure about resolution, tbh. i think thats from like.. the Datalog world??
01:31 <meditans> I don't know, I was skimming a paper about modal logic and it was with backward and forward chaining
01:31 <augur> i dont want to claim that there's a definite answer to the proof search aspects here, this is all open problems
01:32 <meditans> of course; how much difficult is backward chaining, in practice, for the scale of this problem?
01:32 <augur> oh who knows. :)
01:33 <augur> i mean, the code isn't hard
01:34 <meditans> ok, a question about the code, I assume that's written in haskell, or something similar?
01:34 <augur> abstractly, it's just a bunch of cuts backward from an ID proof, if we're doing SEQ, right
01:35 <augur> A => A   is your goal, and you just cut with   P1, P2, ... => A   and so on, until you've killed off all the hypotheses. its basically a context free grammar, really, only you want to be smart when generating possible solutions
01:35 <augur> yeah its all Haskell
01:35 <augur> the current version is VERY primitive, it doesnt do any intention inferring or anything
01:36 <augur> its just that modality stuff. but it also has some more sophisticated linguistic notions
01:36 <meditans> do you use any particular library dealing with the logic part, or did you write everything?
01:36 <augur> when i said Copy(the_file,x) is a simplification, its a HUGE simplification :)
01:36 <augur> i wrote everything from scratch
01:36 <meditans> I can imagine xD
01:37 <augur> wanna see the *actual* meaning of "Copy the file"?  :x
01:37 <meditans> ok, so there isn't a magical package which, if I write the inference rules, will do the backward chaining for me, isn't it xD?
01:37 <augur> no, there isnt :(
01:37 <meditans> yes, of course! xD
01:37 <augur> but writing your own theorem provers is fun practice :)
01:37 <augur> ok here goes. lemme type. see you in a few hours!
01:37 <augur> jk :p
01:37 <meditans> xD
01:37 <•doppioslash> xD
01:38 <•doppioslash> how do planners come in?
01:38 <•doppioslash> ...in the picture
01:41 <augur> ignoring the Imp modality:     require a : Event, _ : Speaker a User, _ : Addressee a Computer, f : Entity, s : Event, _ : File s, _ : Experiencer s f in   (c : Event) * (f' : Entity) * Copy e * Copier e Computer * CopyOriginal e f * CopyResult e f'
01:41 <augur> thats more or less how it goes, after some normalization and solving
01:44 <meditans> that's actually fun to read, for the philosophical honesty of the types xD
01:44 <augur> :p
01:44 <augur> its an event-semantics representation of meaning that uses whats called thematic separation
01:45 <augur> it works really nicely, too, because you can export to a nice JSON rep :)
01:45 <augur> ignoring the requires, which eventually get normalized away, this extracts to just something like
01:45 <meditans> googling thematic separation xD
01:46 <augur> { "isa": "Copy", "copyOriginal": f, "copyResult": f' }
01:46 <augur> thematic separation is these copier/copyorigina/etc things
01:46 <augur> so originally, donald davidson suggested instead of this:   Stab(Brutus,Caesar)
01:46 <augur> you do this:   exists e. Stab(e,Brutus,Caesar)
01:47 <augur> and then castañeda suggested    exists e. Stab(e) & Stabber(e,Brutus) & Stabee(e,Caesar)
01:47 <meditans> what is the semantic for the first place in Stab(e,Brutus,Caesar)?
01:47 <augur> or maybe you have more abstract/generic "thematic roles" -- instead of Stabber maybe you have Agent or whatever
01:47 <augur> its an event
01:47 <augur> e is the stabbing act
01:48 <meditans> ok, makes sense
01:48 <augur> various philosophical and empirical arguments exist to suggest that stuff like that is at the very least, really convenient
01:48 <augur> and possible even absolutely necessary
01:49 <augur> oh, incidentally
01:49 <augur> since modal logic is part of the overall topic in here
01:49 <augur> if you have events and thematic separation and are BRUTAL in using this
01:49 <augur> then you can instead use what's called description logic, which is a multi-modal logic
01:50 <augur> basically, a logic with varieties of <>
01:50 <meditans> yeah, I linked the wikipedia page of multimodalities to doppioslash just before your arrival
01:50 <augur> so:   Stab & <Stabber>Brutus & <Stabbee>Caesar
01:50 <meditans> continue with the example
01:51 <augur> ill leave it there, since thats about it :)
01:51 <augur> doppioslash: planners would presumably be involved in achieving the goals
01:51 <augur> in my system, the planner is just the prover that proves the goal
01:51 <augur> the proof objects being the plans
01:52 <augur> Pfenning and someone else have a paper on this for robotics, too
01:52 <augur> hello anna_!
01:52 <augur> or is it anna__
01:52 <augur> Uluç Saranli and Frank Pfenning. Using constrained intuitionistic linear logic for hybrid robotic planning problems.
01:52 <augur> http://www.cs.cmu.edu/~fp/papers/icra07.pdf
01:53 <anna__> augur: hi augur
01:53 <augur> also, here's *a* GDC video about AI and narrative, but maybe not the one i was remembering
01:53 <augur> http://www.gdcvault.com/play/1012421/AI-and-Interactive-Storytelling-How
01:54 <augur> anyway, so, meditans, thats how LE works right now :p
01:54 <augur> if you saw the video on the page, thats basically how its implemented, modulo grungy details
01:55 <meditans> yeah, I saw the demo, thanks for all the patience required to go through my questions, it was very interesting to me
01:55 <augur> i hope it was. thank you for the patience of sticking with it and not telling me to shut up XD
01:56 <meditans> and that thing that planning is just proving in an opportune modality is inspiring
01:56 <augur> its not narrative-related, but, i think a lot about narrative in similar terms
01:56 <augur> i have various plans for a game with infinite gameplay due to generative plot mechanisms
01:56 <augur> and my usual way of thinking about it is basically in precisely the terms i described above, just on auto-pilot
01:57 <meditans> oh, I got another question, of a more practical nature
01:57 <augur> major actors w/ goals + various actions they can take to achieve them over time, and those break down into smaller and smaller goals, and maybe you'd have other actors getting involved b/c one way of achieving a goal is to ask someone else to do it, etc
01:58 <augur> ok, i might have an answer!
01:58 <augur> but more likely just a perspective :)
01:58 <meditans> I think that could have a great overlap area with what we are envisioning
01:58 <meditans> however, regarding the question xD
01:59 <meditans> let's say I wanted to implement some kind of generic prover to toy with some logics for narrative purposes
01:59 <meditans> what should I read? (papers, articles, ecc)
01:59 <augur> oh boy um
01:59 <meditans> what problems should I expect
02:00 <meditans> hahaha it's a very broad question xD
02:00 <augur> my usual recommendation is to first make sure you're really comfortable with proof theory of the Pfenning sort, by watching his 2012 OPLSS lectures
02:00 <meditans> OPLSS are those made in oregon?
02:00 <augur> yep
02:00 <augur> Oregon Programming Languages Summer School
02:01 <augur> http://purelytheoretical.com/sywtltt.html << i have some links here
02:01 <augur> then, for implementation, i'd suggest first toying around with a naive translation into haskell or your FP lang of choice
02:01 <meditans> oh, I saw the Harper ones, though
02:01 <augur> forget the harper ones for now
02:02 <augur> the pfenning ones are more important
02:02 <augur> 2012 specifically
02:02 <meditans> ok xD
02:02 <augur> frank goes through Natural Deduction, then Sequent Calculus (which is nicer for proving) and then the Focused Calculus (which is even better for proving)
02:03 <augur> type checking is a different beast so ignore anything i wrote on that page that looks like it might relate to type checking
02:04 <augur> frank even mentions chaining directions when he talks about the Polarized version of the focused calculus
02:04 <augur> or wait, maybe the focused calculus *is* polarized?
02:04 <augur> whatever. :)
02:04 <meditans> perfect, I will learn those first xD
02:05 <meditans> I'm confortable with natural deduction, know something about sequent calculus, but never heard about focused calculus
02:05 <meditans> so that should be fun, for now, and then I'll just bug you again for advices xD
02:06 <augur> :)
02:07 <augur> ok thats enough from me. i've dumped a wall of text on everyone, and thats a bit unfair of me
02:07 <•doppioslash> ...well it was interesting
02:07 <•doppioslash> wish I could understand more, but more studying for me I guess
02:07 <augur> http://www.gdcvault.com/play/1017987/Narrative-Generators-Sports-Games-and
02:07 <augur> > Narrative Generators: Sports Games and Story Engines
02:08 <augur> dunno why sports games is there but i guess ill find out!
02:08 <•doppioslash> xD
02:09 <meditans> doppioslash: a nice paper on exclusion logic, to store in the vault xD
02:09 <meditans> https://encrypted.google.com/url?sa=t&rct=j&q=&esrc=s&source=web&cd=1&cad=rja&uact=8&ved=0ahUKEwj_oNStuKrJAhXE8RQKHQ5UB1UQFggcMAA&url=http%3A%2F%2Fphilpapers.org%2Farchive%2FEVAIEL.pdf&usg=AFQjCNEYlFspLkiMrLydSJfqxaplLYFhUQ&sig2=mmTPYHR_HWOY6zxf1EPyeQ
02:10 <•doppioslash> I'm working on a vault xD