Should I allow for non-monotonic reasoning?

[norbert...@gmail.com]

I have been developing the first-order reasoner RACE [1] for Attempto Controlled English ACE [2] that allows users to check the consistency of a set of ACE axioms, to deduce ACE theorems from ACE axioms and to answer ACE queries from ACE axioms.

RACE uses a set of auxiliary axioms to express context-independent knowledge like the relation between plural nouns and singular nouns, or the ordering relations of natural numbers. These auxiliary axioms are written in Prolog that – having the power of the Turing machine – allows us to practically do any deduction. Thus often the question is not "Is this deduction correct?", but "Should RACE allow for this deduction?".

In the following I would like to discuss a case where this question arises.

Using the power of Prolog I have extended RACE by auxiliary axioms that perform second-order deductions, concretely aggregation. Thus RACE can deduce

John is a man. Johnny is a man. ⊢ There are two men.

Adding a further axiom establishing that, in fact, Johnny is John, RACE fails.

John is a man. Johnny is a man. Johnny is John. ⊬ There are two men.

Thus I have a case of non-monotonic reasoning. (Note that RACE can still deduce that there is one man.)

My question to the community is "Should RACE allow for non-monotonic reasoning, or does non-monotonicity have consequences that could confuse RACE users in more complex cases?"

[1] http://attempto.ifi.uzh.ch/race/

[2] http://attempto.ifi.uzh.ch/site/resources/


Norbert E. Fuchs
Department of Informatics & Institute of Computational Linguistics
University of Zurich

[Jan Burse]

norbert...@gmail.com schrieb:

> John is a man. Johnny is a man. ⊢ There are two men.

In FOL the above is not true. Since there can be
a model where John=Johnny and a model where John<>
Johnny.

And of course in FOL there can be a model where
the is_man/1 relation might contain more than
only {John, Johnny} (which can be of cardinality
1 or 2).

So you need closed world assumptions already for
the is_man/1 relation, and then some domain
independence for John and Johnny.

Just to get
?- aggregate_all(count, ..., R)
R = 2

Or what ever the formulation in RACE would be.

But you might have non-monotonicity of |- (first
sense) or non-monotonicity of queries, i.e. queries
which don't have positive polarity (second sense).
Or both.

A query with aggregate_all/3 and friends is
always non-monotonic already in the second sense.
This comes from the ur-form of such predicates, set
comprehension (kind of findall/3):

forall w,x exists y forall z(z in y <-> P(z,w,x) & z in x)
http://en.wikipedia.org/wiki/Axiom_schema_of_specification#Statement

Because of the biconditional <->/2 the comprehended
predicate P/3 occurs in positive and negative position
at the same time.

Its an interesting question what is going on in such
predicates such as aggregate_all/3 logically, which
have become more and more everyday use for Prolog
programming.(*)

Bye

(*)
But still not standardized. Also difficult to find
test suites. But special constructs for it for example
in languages such as Picat.

Like twenty or so years ago, also some research with
datalog that incorporates comprehension, i.e. Zaniolo
etc.. Example paper that came up quickly via Google
search:
http://www.cs.ucla.edu/~zaniolo/papers/pods91.pdf

[Jan Burse]

Jan Burse schrieb:

> Its an interesting question what is going on in such
> predicates such as aggregate_all/3 logically, which
> have become more and more everyday use for Prolog
> programming.(*)

If you go HOL, i.e. higher order logic, you might
have a lot of fun, with forming comprehension as

lambda z.(P(z,w,x) & z in x)

But I guess this is out of scope, since you restricted
your question to FOL.

I have not yet seen much papers giving polarity
to lambda abstraction. On the other hand obviously
lambda abstraction has the same polarity problem
as comprehension.

Nevertheless there are monotonic calculi for lambda
comprehension, but maybe they live in weaker
models of lambda calculus, than the set theory
model of comprehension would suggest, and/or
they take only care of one direction of the
<->/2, i.e. <- and -> separately.

So possibly looking into HOL could eventually
also give semantics to logic programming with
aggregate_all/1 and friends. Some different
semantics than what was explored in the past,
i.e. twenty years ago or so?

Bye

[norbert...@gmail.com]

Jan

Thanks for your detailed answers to which for now I will respond only concerning two aspects of RACE.

On Saturday, 23 May 2015 16:36:54 UTC+2, Jan Burse wrote:
> norbert...@gmail.com schrieb:
> > John is a man. Johnny is a man. ⊢ There are two men.
>
> In FOL the above is not true. Since there can be
> a model where John=Johnny and a model where John<>
> Johnny.
>

Perhaps I should have written that RACE uses the unique name assumption, i.e. "John" and "Johnny" are distinct unless I explicitly define them as identical. Thus there are (at least) two men.

> And of course in FOL there can be a model where
> the is_man/1 relation might contain more than
> only {John, Johnny} (which can be of cardinality
> 1 or 2).
>

Right. Again I should have been clearer, but this didn't seem necessary since my question relates to something else. The deduction that RACE actually generates is

John is a man. Johnny is a man. ⊢ There are at least two men.

since RACE interprets a natural number X as "at least X".

--- nef

[graham...@gmail.com]

That's what I'm working on. However all is a difficult predicate unless we drop extensionality and use induction for equality.

[Jan Burse]

Hi,

Not really related to non-monotonic reasoning,
but related to higher order logic. I had a nice
read on Henkin semantics recently:

Types, Tableaus, and Gödel's God
Melvin Fitting, 31. Dezember 2013

http://www.amazon.de/Types-Tableaus-G%C3%B6dels-Trends-Logic/dp/9401039127

But a popularization of Henkin semantics
began already earlier. For example by this
SEP entry:

Second-order and Higher-order Logic
Herbert Enderton († 2010), 2009
http://plato.stanford.edu/entries/logic-higher-order/

In the Melvin Fitting book there is explicitly
related lambda abstraction and set comprehension.
Actually he gives semantic to lambda abstraction
via set comprehension.

Extensionallity is intially dropped, if I remember
well, whether there is an induction for equality
in Melvin Fittings book as well I don't
remember. Disclaimer: No warranty.

Bye

graham...@gmail.com schrieb: