My previous approach was to preserve this multi-level structure, calling the sequents "rules" and the sequent inference rules "meta-rules" (since they are rules for creating rules). However, it would be more efficient to eliminate the extra level if possible.

In general, this may be a complicated process. Some sequent derivation rules have special syntactical restrictions, such as "... X and Y share no free variables ...". Also consider sequent rules like "If A,B |- C, then A |- (B->C)". It isn't obvious that there is a simple way to turn a specification of a system in terms of sequent derivation rules into a direct specification consisting of inference rules on statements.

Typical systems, though, will obey a few nice properties. First, adding more premises to a valid sequent will always result in a valid sequent. Furthermore, many sequent derivation rules just propagate along the premises from the sequents they start with to the sequents they produce. For sequents which do that, the job is easy. Consider an example:

**"From A, B, C... |- P and D, E, F... |- Q conclude A, B, C... D, E, F... |- (P&Q)"**

In this case, we'd just translate the whole thing to the rule "From P and Q conclude (P&Q)". These sorts can be eliminated from the meta-level immediately, which is good (every little bit helps).

Unfortunately, not all cases are so easy. Many inference rules will

*almost*pass along the premises untouched, but make some little modifications to the list. These modifications will

*usually*be to remove specific premises,

*occasionally*to add premises, and

*quite rarely*to modify the internals of premises. The example above, "If A,B |- C, then A |- (B->C)", is one example of this: one premise is eliminated in the process of drawing the conclusion. Getting rid of meta-rules of this sort requires cleverness.

First-order natural deduction systems handle that particular example in a nice way: at any time during reasoning, we may make a new assumption. This can be anything. We keep the list of assumptions that have been made. Now, say we just concluded something, S. One deduction move we can now make is to remove an assumption from the list (call it A), and stick it on the beginning of S with an arrow: A->S is our new conclusion, which is true in the new context (ie, the old context minus one assumption).

This general idea could be extended to

*any*rules which add or eliminate premises: they are seen as just modifying the list of assumptions.

A practical implementation of this sort of idea for Genifer might be to engage in hypothetical reasoning via conditional queries: we make a query with a list of assumptions attached, to be used in addition to the actual facts. However, some issues may come up with respect to the difference between the classical conditional and the probabilistic conditional. I need to consider this more. (The approach is similar to my "rule-level reasoning", but rather than reasoning about rules using conditional queries, we reason about statements...)

This leaves rules which modify the sequents internally. The primary example of this is variable instantiation, but that's handled by unification! So, in summary, it appears to me that my "meta-level" is not needed in Genifer and can be eliminated with a little patience...

All of the above discussion was done with a translation of HOL Light in mind, but could apply to IG or an IG variant equally well.

I've always seen sequents as representing statements under contexts, and there is always a context to everything. How does Genifer represent contexts? Is there only a single context "here-now-me" so that all reasoning is lifted into explicit contitionals?

ReplyDeleteIn logic, sequents are a dissection of a consequence relation "theory=Cn(assumptions)" i.e. "partial-assumptions |- part-of-theory", but in computer science, different sorts of context indicators are put to the left of turnstyle. For example, in type inference, "Gamma, Phi |- e : t" means that in the context of expression variables having types specified by Gamma and type variables meeting the constraint Phi, "e" has type "t".

@Lukasz:

ReplyDeleteIn my opinion, Genifer should not have explicit contexts in the inference rules. All contexts are represented by propositions; for example, if Genifer is reasoning about physics, then the statement "in_context(physics)" will be true in the KB. In this way, very complex contexts can be represented. Also, we can use forward chaining to *recognize* what context a complex situation belongs to.

Is that the kind of contexts you're thinking about?