handle definitions

[newca12]

From fra...@gmail.com on March 17, 2010 14:19:04

At the moment, LK proofs in gapt support definition introduction rules, but their correctness is not verified.

To change this, we propose to create a DefinitionManager who manages definitions of the form

P(x_1,...,x_n) <-> F(x_1,...,x_n)

where P is a symbol and F is an expression with free variables shown. A DefinitionManager object should be created when creating a proof (e.g. in a parser), and be passed to all definition inferences in the proof. When constructing the inferences, we can then verify correctness of the inference.

Original issue: http://code.google.com/p/gapt/issues/detail?id=73

[newca12]

From bruno...@gmail.com on August 19, 2011 23:20:14

Labels: Component-LogicalDataStructures

[newca12]

From fra...@gmail.com on August 23, 2011 06:48:40

Labels: -Priority-Medium Priority-Low Milestone-Release3.0

[newca12]

From fra...@gmail.com on August 23, 2011 06:49:26

It seems that this was never implemented in the C++ ceres...

[newca12]

From bruno...@gmail.com on August 30, 2011 07:33:46

What if we make a defined symbol be not an atomic symbol, but a "formula link" that points to a formula?

This would make our whole system more homogeneous, since this idea is essentially analogous to "proof links" (something that we already have in some form)... And it would also make it unnecessary to implement a global definition manager... The correctness of definition rules could then be checked locally...

[newca12]

From fra...@gmail.com on August 30, 2011 07:41:35

Good idea! At the moment, though, we do have a ``manager'' for the proof links. The problem seems to be that, when creating a definition (proof schema in this case), the definiendum may occur in the definiens (as is usual in primitive recursive definitions). To avoid this circularity, I introduced this manager.

It may well be possible to solve this problem without it, though (e.g. by creating definitions using a single "special" symbol, that will be replaced by the definiendum when the structure of the definiens is completely specified. This approach may not work for mutually recursive definitions, though...).

I agree that a homogeneous approach would be best! Now seems like a good time to think about it.

[newca12]

From Martin.R...@googlemail.com on December 19, 2011 04:37:23

Owner: Martin.R...@googlemail.com

[newca12]

From fra...@gmail.com on March 12, 2013 01:26:30

To fix the performance problems of proof skolemization, it seems to me that I now need to deal with definitions (to compute, in proof skolemization, the exact structure of Skolem symbols in a formula modulo definitions).

Cvetan has already implemented a DB for rewrite rules in schema.scala. Unfortunately it presupposes that definitions are given in the form (base, step).

I'd like to generalize this code by storing in the DB general rewrite rules s -> t and move this to a more prominent place outside of the schema code, and use it in the following way:

1) Parse definitions from an XML proof into the DB. 2) Normalize HOLExpressions w.r.t. the rewrite rules in the DB.

I believe that will allow us to handle the definitions we are using so far in both schemata and proofs like the prime proof.

What do you think?

Also, there is the object at.logic.algorithms.rewriting.defintion_elimination which seems to accomplish 2). I cannot find any tests or other uses of the algorithm in gapt. Could someone maybe comment on the status of this code?

Cc: cdunc...@gmail.com stefan.hetzl olivier....@edla.org

[newca12]

From cdunc...@gmail.com on March 18, 2013 00:35:01

Hi Daniel, I think that such a generalization and removing the rewriting part from schema not a bad idea. If you want I can help you with the programming. We can have a meeting to discuss it. Also we had a discussion with Martin about the DB's. Now most of them are objects and no instances are possible.

Owner: cdunc...@gmail.com

[shetzl]

adding CCs from google code: @shetzl @newca12

[gebner]

This is now implemented in the Context class, see #561 for the current discussion on more general definitions.