Outermost - Revision history

Gnaedig: /* Participants */

2008-11-25T17:27:42Z

Participants

2008-11-17T10:17:27Z

Overview of the Event

2008-11-14T12:26:07Z

2008-11-07T16:02:59Z

Problem selection

2008-11-07T16:00:50Z

Scoring

2008-11-07T15:51:31Z

Overview of the Event

2008-11-03T15:40:24Z

2008-11-03T11:31:51Z

Problem selection

2008-11-03T10:58:09Z

2008-11-03T09:33:33Z

Problem selection

@@ Line 79: / Line 79: @@
 * AProVE-team
 * Matthias Raffelsieper, Hans Zantema
 * Christian Sternagel and Rene Thiemann (TTT2)
 * Joerg Endrullis (Jambox)
 * Johannes Waldmann (Matchbox), but will need more time

@@ Line 26: / Line 26: @@
 * René Thiemann:
 I would also prefer the outermost variant, since currently some methods (for disproving) are only correct for outermost termination and not for outermost ground termination. Moreover, by extending the signature every tool that only can prove outermost ground termination can also prove outermost termination.
 == Problem selection ==

← Older revision		Revision as of 12:26, 14 November 2008
Line 23:		Line 23:

	is ground outermost terminating (when restricting to symbols occurring in the TRS), but not outermost terminating if we allow open terms or allowed to extend the signature. Since the open variant is more robust (it does not change by extending the signature) I propose to allow open terms in the definition of outermost termination, by which the above example is NOT outermost terminating.		is ground outermost terminating (when restricting to symbols occurring in the TRS), but not outermost terminating if we allow open terms or allowed to extend the signature. Since the open variant is more robust (it does not change by extending the signature) I propose to allow open terms in the definition of outermost termination, by which the above example is NOT outermost terminating.
		+
		+	* René Thiemann:
		+
		+	I would also prefer the outermost variant, since currently some methods (for disproving) are only correct for outermost termination and not for outermost ground termination. Moreover, by extending the signature every tool that only can prove outermost ground termination can also prove outermost termination.

	== Problem selection ==		== Problem selection ==

← Older revision		Revision as of 16:02, 7 November 2008
Line 33:		Line 33:
	* Hans Zantema:		* Hans Zantema:

−	I agree with Joerg that apart from these TRSs where full termination has not already been proven special TRSs with outermost strategy should be considered. Giving both of these subcategories equal weight is OK with me. The main point to be done now is to extend the present list of only 6 TRSs in TPDB with outermost strategy. ~~I intend to submit some new systems; I hope other participants will do that too.~~ A competiton does not make sense before this list has some reasonable size and content.	+	I agree with Joerg that apart from these TRSs where full termination has not already been proven special TRSs with outermost strategy should be considered. Giving both of these subcategories equal weight is OK with me. The main point to be done now is to extend the present list of only 6 TRSs in TPDB with outermost strategy. A competiton does not make sense before this list has some reasonable size and content.
		+
		+	A proposal for 50 new examples is found in http://www.win.tue.nl/~hzantema/ex.zip. It is my intension to submit these. If you have remarks, or suggestions for extensions, please let me know.

@@ Line 11: / Line 11: @@
 where programming with infinite structures is common practice and
 therefore full termination (with respect to an arbitrary strategy) cannot be expected.
 == Problem selection ==

@@ Line 57: / Line 57: @@
 insert your name here if you intend to participate.
+* AProVE-team
 * Olivier Fissore, Isabelle Gnaedig, Hélène Kirchner (Cariboo)
 * Matthias Raffelsieper, Hans Zantema

← Older revision		Revision as of 11:31, 3 November 2008
Line 22:		Line 22:

	I agree with Joerg that apart from these TRSs where full termination has not already been proven special TRSs with outermost strategy should be considered. Giving both of these subcategories equal weight is OK with me. The main point to be done now is to extend the present list of only 6 TRSs in TPDB with outermost strategy. I intend to submit some new systems; I hope other participants will do that too. A competiton does not make sense before this list has some reasonable size and content.		I agree with Joerg that apart from these TRSs where full termination has not already been proven special TRSs with outermost strategy should be considered. Giving both of these subcategories equal weight is OK with me. The main point to be done now is to extend the present list of only 6 TRSs in TPDB with outermost strategy. I intend to submit some new systems; I hope other participants will do that too. A competiton does not make sense before this list has some reasonable size and content.
		+
		+
		+
		+	* Joerg Endrullis:
		+
		+	Yes, I will add some more examples to the outermost category. Unfortunately the search in the termination competition interface does not work. Searching for outermost examples yields always the empty result, such that one cannot see which examples are already there.

	== Scoring ==		== Scoring ==

@@ Line 16: / Line 16: @@
 * René Thiemann suggests:
-all TRSs where full termination has not already been proven.
+All TRSs where full termination has not already been proven. If there is a special category of "interesting" outermost-examples then I suggest to add all non-terminating TRSs to this category. The reason is that these examples are interesting since only provers which are aware of the outermost-strategy can solve these examples.
@@ Line 42: / Line 42: @@
 * (number of problems solved) / (number of problems solved by winner).
 Thus in theory a tool winning both categories obtains 100 points.
 == Participants ==
@@ Line 50: / Line 54: @@
 * Olivier Fissore, Isabelle Gnaedig, Hélène Kirchner (Cariboo)
 * Matthias Raffelsieper, Hans Zantema
-* Rene Thiemann (TTT)
+* Christian Sternagel and Rene Thiemann (TTT2)
 * Joerg Endrullis (Jambox)
 * Johannes Waldmann (Matchbox), but will need more time