I'm ending this branch of the discussion. We aren't communicating well enough for it to be worthwhile. To be more specific, I'm not going to reply to any of your emails about logic. Just assume I have an issue with everything you've said, which isn't far from the truth.
On Fri, Apr 3, 2015 at 2:26 PM, Keean Schupke <[email protected]> wrote: > 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. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
