Binding of variables not working correctly for exceptions

[pallix]

Hi,

In the following example I would expect the universal argument to be undercut. Instead, one of the premise of the undercutter is p is not true for _G59032, which seem to indicate a bug in the binding of the variables.

When notTrueFor is defined to be unary, it works. However it makes little sense to have notTrueFor being unary in this model.

meta:
  title: Universal quantification

language:
  exists/2: "∃ %s, %s(of-it) is true"
  belongs/2: "%s belongs to a set of values that make %s true"
  universal/1: "∀ x, %s(x) is true"
  belongs/2: "%s belongs to a set of values that make %s true"
  defined/1: "%s is defined"
  postulatedAsTautology/1: "We postulate %s is a tautology "
  notTrueFor/2: "%s is not true for %s"

argument_schemes:

  - id: universal
    meta:
      note: >
        ∀ x, P(x) is true
    variables: [P,X]
    conclusions:
      - universal(P)
    premises:
      - postulatedAsTautology(P)
    exceptions:
      - notTrueFor(P,X)

statements:
  universal(p1): ∀ x, p1(x) is true
  universal(p2): ∀ x, p2(x) is true

assumptions:
  - postulatedAsTautology(p)
  - notTrueFor(p,x)

[tfgordon]

Exceptions may not use variables which are not used in some premise. That is, all the exceptions

need to be ground when the argument is constructed by matching and instantiating the premises.

Ditto for the conclusions and assumptions.

It seems you would like to represent inference rules for quantifiers in predicate logic.

I do not think that Constraint Handling Rules, the basis for the argumentation schemes language

in this version of Carneades, is expressive enough to represent inference rules for quantifiers.

But it might be interesting to try to find some encoding which works.

p.s. The validator needs to be extended to check for new variables in the exceptions, conclusions

and assumptions, and also to check for declared variables which are not used anywhere. I will

post a new issue for this.

[tfgordon]

That said, I have an idea about how to modify the translation of schemes into CHR rules which would allow additional variables in exceptions, as in your example. Do you see a need for this feature?

[pallix]

Not sure. I will get back to you if we need it.