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 techniques 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.

34 pages

This document was written as a project report for 15-819K Logic Programming, taught by Frank Penning in Fall 2006.

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu