Sciweavers

Share
ENTCS
2008

Focusing the Inverse Method for LF: A Preliminary Report

10 years 2 months ago
Focusing the Inverse Method for LF: A Preliminary Report
In this paper, we describe a proof-theoretic foundation for bottom-up logic programming based on uniform proofs in the setting of the logical framework LF. We present a forward uniform proofs calculus which is a suitable foundation for the inverse method for LF and prove its correctness. We also present some preliminary results of an implementation for the Horn Fragment as part of the logical framework Twelf, and compare its performance with the tabled logic programming engine.
Brigitte Pientka, Xi Li, Florent Pompigne
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Where ENTCS
Authors Brigitte Pientka, Xi Li, Florent Pompigne
Comments (0)
books