BUG: kbr-1 is ill-formed

[mereolog]

Describe the bug
The CLIF axiom kbr-1 is ill-formed.

To Reproduce

BFO-2020/src/common-logic/continuant-mereology.cl

Lines 73 to 77 in 25c834e

	(cl:comment "If a continuant-part-of b then if a is an instance of spatial-region then b is an instance of spatial-region, and vice-versa [kbr-1]"
	(forall (p q t)
	(if (continuant-part-of p q t)
	(iff (instance-of p spatial-region t)
	(and (instance-of q spatial-region t))))))

The syntax problem is with the conjunction, which as it is now, has only one argument, but I suspect that the whole axiom needs to be rewritten as it does not corresponds to its elucidation in the comment.

[michaelrabenberg]

I assume it should just be revised to get rid of the "and," as follows:

(cl:comment "If a continuant-part-of b then if a is an instance of spatial-region then b is an instance of spatial-region, and vice-versa [zzz-1]"
(forall (p q t)
(if (continuant-part-of p q t)
(iff (instance-of p spatial-region t)
(instance-of q spatial-region t)))))

That captures my reading of the comment.

[alanruttenberg]

The and is unsightly but legal I believe:

boolsent = ( open, ('and' | 'or') , { sentence }, close ) | ( open, ('if' | 'iff') , sentence , sentence, close ) | ( open, 'not' , sentence, close ;

sentence is surrounded by curly braces which is zero or more in EBNF. also

6.1.1.14 A Boolean sentence has a type, called a connective, and a number of sentences called the components of the Boolean sentence. The number depends on the particular type. The abstract syntax distinguishes five types of Boolean sentences: conjunctions and disjunctions, which have any number of components,...

The semantics is harder for me to assess

I(E) = true if I(C1) = ... = I(Cn) = true; otherwise, I(E) = false

I'm not sure what this means if there's only c1 though it would be odd to allow a single conjunct but consider the conjunction false.

I did a pass at some point trying to remove the superfluous and/or which are a consequence of using macros to generate some of the formulas. I'll see about removing this one, though if we agree it is legal I won't prioritize it.

[alanruttenberg]

In any case, fixed in the next release

[mereolog]

You are right, CLIF does allow 1- and 0-arguments conjunctions, so syntactically kbr-1 is correct.