On Mar 14, 5:39 pm, Jan Burse <janbu...@fastmail.fm> wrote: > Graham Cooper schrieb: > > > If TRUE(x) doesn't work, what is NOT(NOT(x)) ?? > > When modeling inferences, especially in Prolog, I > usually prefer the following verbs: > > solve/1: Like in the vanilla interpreter for > Prolog > thm/1: Like many logical frameworks do. > pos/1 and neg/1: If you have polarity.
where does proof() fit in?
*TRACE MODE* ?
> > Using true/1 is not wrong, but it has the Tarski > limitation like the other verbs, and any verb you > would use, always have. > > > This doesn't mean that you Graham Cooper, > > with your Prolog, cannot derive some > > truths. But you will not be able to derive > > all truths. > > Right? Except for propositional logic, where > you can build complete inference engines, as > soon as you have a little FOL, nada.