2012/11/28 by Keehang Kwon, Kwon, Keehang, Mi-Young Park +1 · 2 citations
Computer Science · #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.LO #cs.PL
paper · pdf · doi:10.48550/arxiv.1211.6535
8 pages. It describes two execution models for interactive logic programming
arxiv created 2015/07/01 · arxiv updated 2015/07/02
Linear logic programming uses provability as the basis for computation. In the operational semantics based on provability, executing the additive-conjunctive goal G1 & G2 from a program P simply terminates with a success if both G1 and G2 are solvable from P. This is an unsatisfactory situation, as a central action of & -- the action of choosing either G1 or G2 by the user -- is missing in this semantics. We propose to modify the operational semantics above to allow for more active participation from the user. We illustrate our idea via muProlog, an extension of Prolog with additive goals.