On 3 April 2015 at 18:39, Matt Oliveri <[email protected]> wrote: > > The logical framework is a logic in a technical sense, but it's not > designed for proving things. In that sense it's not a logic. It's > designed for defining logics. LF is the metalanguage for a logic of > your choice. >
Okay so I am probably misusing the term LF. I mean specifically an intuitionistic logic, from which sound proofs can be derived. No, that's accurate, but you're arguing for my side, because Prolog > can't prove very much about math either. > Well, I don't mean "Prolog", I mean a prolog like language with sound unification, negation-elimination (complete inference) and a proper search method (iterative-deepening). I am using LF to refer to a specific type system implemented by Twelf. > Perhaps you are just using it as an acronym for logical framework? > (Any logical framework?) > Yes, my mistake I am just using LF as an abbreviation for logical-framework. Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
