Mode, Reduction, and Termination Analysis for LolliMon

LolliMon [10] is a linear logic programming language that combines backward-chaining, backtracking semantics for the asynchronous connectives and forward-chaining, committed choice for the synchronous connectives. Mode, reduction, and termination properties are important correctness criteria that can be verified automatically of both backward-chaining and forward-chaining logic programs by establishing suitable moding and subterm relationships between a clause’s head and its subgoals. This work combines existing tech-niques for termination checking of backward-chaining higher-order intuitionistic logic programs and complexity analysis of forward-chaining first-order logic programs, by devising mode, reduction, and termination analyses for the linear logic programming setting in LolliMon. Note: This document was written as a project report for 15-819K Logic Programming taught by Frank Pfenning in the fall of 2006