RE: Is n3 a rules language or a logic language?

From: Wagner, G.R. <G.R.Wagner@tm.tue.nl>
Date: Thu, 5 Sep 2002 19:17:21 +0200
Message-ID: <AA2E843B3FC96349BF60350202650BE92571D2@tmex1.tm.tue.nl>
To: "'Peter F. Patel-Schneider'" <pfps@research.bell-labs.com>, sandro@w3.org

```
> On the other hand
>
> 	a
> 	---
> 	b
>
> is a different rule of inference, which should be read as
> ``If you have concluded a then you can conclude b.''

This is, of course, not a rule of inference in the normal
sense of a valid inference pattern (justified by the fact
that all models of the premise satisfy the conclusion).
We better call it a "material rule" or a "derivation rule".
There is a type of logical formalism, sequent calculi, where
such rules are called "sequents".

>> A logical reasoner knowing one particular rule (which I think is
>> "modus ponens": A, A->B |- A) will do the same thing given "p->q" as a
>> rules engine would if it were given "p |- q".  In fact, a reasoner
>> using any other sound and sufficiently-complete set of inference rules
> > would act the same given "p->q" as a rules engine would with "p |- q".
>
> This is definitely not true.  A rules engine with p |- q will not conclude
> anything from not q whereas a complete reasoner for the propositional
> calculus will conclude not a from not b and a implies b.

I disagree. Sandro is right. The models of the sequent "p |- q" are
exactly the same models as those of the corresponding implication
"p->q", so both expressions entail the same logical consequences
according to their model-theoretic semantics - at least in standard
logics such as classical and intuitionistic logic. But, and here
comes the but, not so in certain nonmonotonic logics, such as the
logic underlying normal logic programs (with negation-as-failure).