Termination-Portal.org - User contributions [en]

People:Peter Schneider-Kamp

2012-11-28T09:17:25Z

Nowonder:

{{Person
|firstname=Peter
|middlenames=
|lastname=Schneider-Kamp
|titles=
|email=petersk@imada.sdu.dk
|homepage=http://imada.sdu.dk/~petersk/
|country=Denmark
|university=University of Southern Denmark, Odense
|department=Department of Mathematics and Computer Science
|role=Associate Professor 
}}



[http://imada.sdu.dk/~petersk/ http://imada.sdu.dk/~petersk/petersk_floc2010.jpg]

People:Peter Schneider-Kamp

2012-11-28T09:17:02Z

Nowonder:

WST

2009-12-16T14:50:03Z

Nowonder:

The International Workshop on Termination (WST) has been held in St. Andrews (1993), La Bresse (1995), Ede (1997), Dagstuhl (1999), Utrecht (2001), Valencia (2003), Aachen (2004), Seattle (2006), Paris (2007), and Leipzig (2009).
WST traditionally brings together, in an informal setting, researchers interested in all aspects of termination, whether this interest be practical or theoretical, primary or derived. The workshop also provides a ground for cross-fertilisation of ideas from term rewriting and from the different programming language communities.

Upcoming events:
* [http://imada.sdu.dk/~petersk/WST2010/ 11th International Workshop on Termination, Edinburgh, 2010]

Information about previous workshops can be found online:
* [http://www.imn.htwk-leipzig.de/wst09/ 10th International Workshop on Termination, Leipzig, 2009]
* [http://www.lsv.ens-cachan.fr/rdp07/wst.html 9th International Workshop on Termination, Paris, 2007]
* [http://www.easychair.org/FLoC-06/WST.html 8th International Workshop on Terminaton, Seattle, 2006]
* [http://www-i2.informatik.rwth-aachen.de/WST04/ 7th International Workshop on Terminaton, Aachen, 2004]
* [http://www.dsic.upv.es/~rdp03/wst/ 6th International Workshop on Terminaton, Valencia, 2003]
* [http://www.cs.tau.ac.il/~nachumd/wst/index.html 5th International Workshop on Terminaton, Utrecht, 2001]
* [http://verify.rwth-aachen.de/giesl/WST99.html 4th International Workshop on Terminaton, Dagstuhl, 1999]
* [http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 3rd International Workshop on Termination, Ede, 1997]
* 2nd International Workshop on Termination, La Bresse, 1995
* 1st International Workshop on Termination, St. Andrews, 1993
Independently from WST, there are meetings on Certified Termination : [[WScT]]

WST

2009-12-16T14:48:17Z

Nowonder:

The International Workshop on Termination (WST) has been held in St. Andrews (1993), La Bresse (1995), Ede (1997), Dagstuhl (1999), Utrecht (2001), Valencia (2003), Aachen (2004), Seattle (2006), and Paris (2007).
WST traditionally brings together, in an informal setting, researchers interested in all aspects of termination, whether this interest be practical or theoretical, primary or derived. The workshop also provides a ground for cross-fertilisation of ideas from term rewriting and from the different programming language communities.

Upcoming events:
* [http://imada.sdu.dk/~petersk/WST2010/ 11th International Workshop on Termination, Edinburgh, 2010]

Information about previous workshops can be found online:
* [http://www.imn.htwk-leipzig.de/wst09/ 10th International Workshop on Termination, Leipzig, 2009]
* [http://www.lsv.ens-cachan.fr/rdp07/wst.html 9th International Workshop on Termination, Paris, 2007]
* [http://www.easychair.org/FLoC-06/WST.html 8th International Workshop on Terminaton, Seattle, 2006]
* [http://www-i2.informatik.rwth-aachen.de/WST04/ 7th International Workshop on Terminaton, Aachen, 2004]
* [http://www.dsic.upv.es/~rdp03/wst/ 6th International Workshop on Terminaton, Valencia, 2003]
* [http://www.cs.tau.ac.il/~nachumd/wst/index.html 5th International Workshop on Terminaton, Utrecht, 2001]
* [http://verify.rwth-aachen.de/giesl/WST99.html 4th International Workshop on Terminaton, Dagstuhl, 1999]
* [http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 3rd International Workshop on Termination, Ede, 1997]
* 2nd International Workshop on Termination, La Bresse, 1995
* 1st International Workshop on Termination, St. Andrews, 1993
Independently from WST, there are meetings on Certified Termination : [[WScT]]

People:Peter Schneider-Kamp

2009-04-20T04:34:09Z

Nowonder:

{{Person
|firstname=Peter
|middlenames=
|lastname=Schneider-Kamp
|titles=
|email=petersk@imada.sdu.dk
|homepage=http://schneider-kamp.de/
|country=Denmark
|university=University of Southern Denmark, Odense
|department=Department of Mathematics and Computer Science
|role=Assistant Professor 
}}



[http://schneider-kamp.de/ http://imada.sdu.dk/~petersk/petersk.jpg]

People:Peter Schneider-Kamp

2009-02-23T22:37:03Z

Nowonder:

{{Person
|firstname=Peter
|middlenames=
|lastname=Schneider-Kamp
|titles=
|email=petersk@imada.sdu.dk
|homepage=http://schneider-kamp.de/
|country=Denmark
|university=University of Southern Denmark, Odense
|department=Department of Mathematics and Computer Science
|role=Assistant Professort 
}}



[http://schneider-kamp.de/ http://imada.sdu.dk/~petersk/petersk.jpg]

User talk:Polytool

2008-11-27T10:21:26Z

Nowonder: Welcome!

'''Welcome to ''Termination-Portal.org''!''' We hope you will contribute much and well.
You will probably want to read the [[Help:Contents|help pages]]. Again, welcome and have fun! [[User:Nowonder|Nowonder]] 10:21, 27 November 2008 (UTC)

Termination Portal

2008-11-10T09:08:38Z

Nowonder: commented publications listing as this is not up to date at all

Termination is a fundamental topic in computer science. While classical results state the undecidability of various termination problems, automated methods have successfully been developed that prove termination or non-termination in practical cases.
Research in termination analysis offers many challenges both in theory (mathematical logic, proof theory) and practice (software development, formal methods).

This portal aims to provide the research community with up-to-date information about the field
of termination analysis.
The main sections are [[:Category:People|People]] (information about researchers in termination analysis),
[[:Category:News|News]] (information about events and new publications),
[[:Category:Tools|Tools]] (information about tools for automated termination analysis), and
[[:Category:Bibtex|References]] (publications related to termination analysis).
Additionally, the portal provide information about past and future [[WST|workshops]] and [[Termination Competition|competitions]].

How to [[Contribute]] to this web resource. -- [[TODO|Suggestions and Corrections]].

=Recent News=
<dpl>
category=News
shownamespace=false
count=10
ordermethod=lastedit
order=descending
includepage={News}:date:text
format =,,\n,
table =class="wikitable",Caption,Date,Text
tablerow =|%%
</dpl>
Older news entries can be found on the [[:Category:News|news page]].

Poll:Test

2008-11-02T07:45:24Z

Nowonder:

<poll>
Test Poll
This poll is nice.
No one likes this poll.
Polly want crackers!
</poll>

Poll:Test

2008-11-02T07:07:23Z

Nowonder:

<poll>
Test Poll
This poll is nice.
No one likes this poll.
Polly want crackers!
</poll>
<poll>STATS
Test Poll
This poll is nice.
No one likes this poll.
Polly want crackers!
</poll>
<poll>CROSS
Test Poll
This poll is nice.
No one likes this poll.
Polly want crackers!
</poll>

Poll:Test

2008-11-02T07:06:27Z

Nowonder:

<poll>
Test Poll
This poll is nice.
No one likes this poll.
Polly want crackers!
</poll>
<poll>STATS
Test Poll
This poll is nice.
No one likes this poll.
Polly want crackers!
</poll>
<poll>REMAINING
Test Poll
This poll is nice.
No one likes this poll.
Polly want crackers!
</poll>

Poll:Test

2008-11-02T07:05:56Z

Nowonder:

<poll>
Test Poll
This poll is nice.
No one likes this poll.
Polly want crackers!
</poll>
<poll>
Test Poll
STATS
This poll is nice.
No one likes this poll.
Polly want crackers!
</poll>
<poll>
Test Poll
REMAINING
This poll is nice.
No one likes this poll.
Polly want crackers!
</poll>

Poll:Test

2008-11-02T07:05:35Z

Nowonder:

<poll>
Test Poll
This poll is nice.
No one likes this poll.
Polly want crackers!
</poll>
<poll>
STATS
Test Poll
This poll is nice.
No one likes this poll.
Polly want crackers!
</poll>
<poll>
REMAINING
Test Poll
This poll is nice.
No one likes this poll.
Polly want crackers!
</poll>

Poll:Test

2008-11-02T06:55:46Z

Nowonder: New page: <poll> Test Poll This poll is nice. No one likes this poll. Polly want crackers! </poll>

<poll>
Test Poll
This poll is nice.
No one likes this poll.
Polly want crackers!
</poll>

Logic Programming

2008-10-29T16:22:50Z

Nowonder:

This page is to record the current status of discussion
on cleaning up the Logic Programming Category of the Termination Competition.

(Discussion should take place on the termtools mailing list.)

== Syntax/Semantics for Input/Output ==

The set of queries, for which termination should be analyzed, is
given by a comment in the first line. Example:

%query: p(i,o).

This means all queries :- p(s,t). where s is a ground term
and t can be any term.

== Problematic Examples ==

The following examples are empty:
* LP/talp/apt/dc_mod.pl
* LP/talp/apt/gt_mod.pl

The following examples contain non-trivial built-in predicates that are potentially
handled in very different ways by the individual tools (leading to potentially
different termination status):
* LP/lpexamples/factorial.pl
* LP/lpexamples/fib-oi.pl
* LP/lpexamples/fib.pl
* LP/lpexamples/hanoi.pl
* LP/lpexamples/kay4.pl
* LP/lpexamples/numbervars.pl
* LP/lpexamples/primes.pl
* LP/lpexamples/tautology.pl
* LP/lpexamples/totient.pl
* LP/talp/apt/curry_ap.pl
* LP/talp/apt/dc_mod.pl
* LP/talp/apt/dc_schema.pl
* LP/talp/apt/gt_mod.pl
* LP/talp/apt/gtsolve.pl
* LP/talp/apt/mergesort_ap_variant.pl
* LP/talp/maria/aiakl.pl
* LP/talp/maria/ann.pl
* LP/talp/maria/bid.pl
* LP/talp/maria/boyer.pl
* LP/talp/maria/browse.pl
* LP/talp/maria/deriv-oii.pl
* LP/talp/maria/deriv.pl
* LP/talp/maria/fib.pl
* LP/talp/maria/grammar.pl
* LP/talp/maria/grammar2.pl
* LP/talp/maria/hanoiapp.pl
* LP/talp/maria/mmatrix.pl
* LP/talp/maria/money.pl
* LP/talp/maria/occur.pl
* LP/talp/maria/peephole.pl
* LP/talp/maria/progeom.pl
* LP/talp/maria/qplan.pl
* LP/talp/maria/qsortapp.pl
* LP/talp/maria/query.pl
* LP/talp/maria/rdtok.pl
* LP/talp/maria/read.pl
* LP/talp/maria/serialize.pl
* LP/talp/maria/tak.pl
* LP/talp/maria/tictactoe.pl
* LP/talp/maria/warplan.pl
* LP/talp/taboch/permute2.pl
* LP/talp/taboch/queens.pl
* LP/terminweb/old-terminweb/mergesort.pl
* LP/terminweb/old-terminweb/queens.pl
* LP/terminweb/old-terminweb/quicksort.pl

== Questions ==

* should empty examples be removed?
* how to handle built-ins that the tool does not support?
* do we want to have a (sub-)category "pure logic programs"?

== Participants ==

The following is a list of participants to this category
* [[Tools:AProVE]]

News:Logic Programming Category of the Termination Competition

2008-10-29T16:18:07Z

Nowonder: New page: <!-- Please insert the corresponding information below so that the news page can be generated automatically. Line breaks are allowed! You may use MediaWiki syntax here to link to...

Logic Programming

2008-10-29T16:16:45Z

Nowonder:

Logic Programming

2008-10-29T16:08:42Z

Nowonder: New page: This page is to record the current status of discussion on cleaning up the Logic Programming Category of the Termination Competition. (Discussion should take place on the termtools maili...

User talk:Hirokawa

2008-10-28T13:10:00Z

Nowonder: Welcome!

User talk:Aschnabl

2008-07-18T07:44:05Z

Nowonder: Welcome!

User talk:Georg.moser

2008-07-17T13:37:49Z

Nowonder: Welcome!

User talk:Slucas

2008-05-19T13:57:29Z

Nowonder: Welcome!

User talk:Hofbauer

2008-05-19T13:56:59Z

Nowonder: Welcome!

User talk:Binabik

2008-05-14T11:03:52Z

Nowonder: Welcome!

User talk:Pierre.Lescanne

2008-05-05T06:04:48Z

Nowonder: Welcome!

Bibtex:GSST06

2008-04-08T06:23:03Z

Nowonder: New page:  == BibTex ==  <bibtex> ...

[[Category:Bibtex| ]]
[[Category:BibtexNews| ]] 
== BibTex ==

<bibtex>
@inproceedings{RTA06,
author = "J. Giesl and S. Swiderski and P. Schneider-Kamp and R. Thiemann",
title = "Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages",
booktitle = "Proceedings RTA '06",
publisher = "Springer",
series = "LNCS 4098",
pages = "297-312",
year = "2006"
}
</bibtex>

News:Adding References

2008-04-08T05:57:45Z

Nowonder:

{{News
|text='''Harald''': Is there a general format which one should use when adding (one's) publications? I think that should be fixed soon in order to ensure a uniform layout.

'''Peter''': If you refer to choosing the Identifier, I would propose name+year[+a-z] for single author papers
and initials+year[+a-z] for multi author papers. If you refer to the reference itself, the usual BibTeX formats should be supported.
|date=April 7, 2008
}}

News:Adding References

2008-04-08T05:57:21Z

Nowonder:

{{News
|text='''Harald''': Is there a general format which one should use when adding (one's) publications? I think that should be fixed soon in order to ensure a uniform layout.

'''Peter''': If you refer to the choosing the Identifier, I would propose name+year[+a-z] for single author papers
and initials+year[+a-z] for multi author papers. If you refer to the reference itself, the usual BibTeX formats should be supported.
|date=April 7, 2008
}}

News:Domain Registered

2008-04-07T15:08:11Z

Nowonder:

{{News
|text=The domain [http://termination-portal.org/ termination-portal.org] has been registered and should be propagated to all nameservers within 48 hours. It already works from here.
|date=Apr 7, 2008
}}

News:Domain name

2008-04-07T15:07:33Z

Nowonder:

{{News
|text=[[What domain name?]] (Poll, closed)
|date=March 31, 2008
}}

News:Termination Portal Online

2008-04-07T15:07:06Z

Nowonder:

{{News
|text=The Termination Portal is online for testing. Please find and report any bugs (except for the ants).

Note: Replace "Firstname Lastname" or "Tool Name" by your name or the name of your tool for correct listing.
|date=March 29, 2008
}}

News:Domain Registered

2008-04-07T15:06:33Z

{{News
|text=The domain "termination-portal.org" has been registered and should be propagated to all nameservers within 48 hours. It already works from here.
|date=Apr 7, 2008
}}

Tools:TTT2

2008-04-01T09:45:45Z

Nowonder:

{{Tool
|shortname= TTT2
|longname= Tyrolean Termination Tool 2
|homepage= http://colo6-c703.uibk.ac.at/ttt2
|country= Austria
|university= Innsbruck
|developers= Martin Korp, [[People:Christian Sternagel|Christian Sternagel]], [[People:Harald Zankl|Harald Zankl]], and Aart Middeldorp
}}

What domain name?

2008-03-31T12:31:38Z

Nowonder:

We want to have a domain name for this web site.
What is your preference? Vote here

* termination-portal.org

* termination-live.org (by analogy to satlive.org)

or extend the list (but check that the name is free).
(everything like termination.* seems already taken)

Peter: I like termination-portal as it is descriptive.

People:Stephan Swiderski

2008-03-31T07:25:50Z

Nowonder:

{{Person
|firstname=Stephan
|middlenames=
|lastname=Swiderski
|titles=
|email=swiderski@informatik.rwth-aachen.de
|homepage=http://verify.rwth-aachen.de/swiderski/
|country=Germany
|university=RWTH Aachen
|department=Research Group Computerscience II
|role=PhD Student
}}

People:Peter Schneider-Kamp

2008-03-30T11:43:19Z

Nowonder:

{{Person
|firstname=Peter
|middlenames=
|lastname=Schneider-Kamp
|titles=
|email=psk@informatik.rwth-aachen.de
|homepage=http://schneider-kamp.de
|country=Germany
|university=RWTH Aachen
|department=Research Group Computer Science 2
|role=Research and Teaching Assistant 
}}



[http://verify.rwth-aachen.de/psk/ http://verify.rwth-aachen.de/psk/psk.jpg]

Tools:AProVE

2008-03-30T11:42:12Z

Nowonder:

{{Tool
|shortname=AProVE
|longname=Automated Program Verification Environment
|homepage=http://aprove.informatik.rwth-aachen.de
|country=Germany
|university=RWTH Aachen
|developers=Jürgen Giesl, [[People:René Thiemann|René Thiemann]], [[People:Peter Schneider-Kamp|Peter Schneider-Kamp]], Stephan Swiderski, [[People:Carsten Fuhs|Carsten Fuhs]] et al.
}}

People:René Thiemann

2008-03-29T21:35:17Z

Nowonder:

{{Person
|firstname=René
|middlenames=
|lastname=Thiemann
|titles=
|email=rene.thiemann@uibk.ac.at
|homepage=http://cl-informatik.uibk.ac.at/~thiemann/
|country=Austria
|university=University of Innsbruck
|department=Computational Logic Group
|role= 
}}

Tools:TALP

2008-03-29T21:22:22Z

Nowonder: New page: <!-- Please fill in the data so that your tool can be added to some default categories and a simple tool page can be created. You may extend that tool page yourself af...

{{Tool
|shortname=TALP
|longname=Termination Analysis of Logic Programs
|homepage=http://bibiserv.techfak.uni-bielefeld.de/talp/
|country=Germany
|university=University of Bielefeld
|developers=Enno Ohlebusch
}}



----

TALP uses a transformation from well-moded logic programs to term rewrite systems. The details of this
transformation are described in [[:Bibtex:Ohlebusch01]]. For non-well-moded logic programs, a more recent
transformation is described in [[:Bibtex:SGST06]].

Bibtex:Ohlebusch01

2008-03-29T21:10:29Z

Nowonder:

<bibtex>

@article{Ohlebusch01,
AUTHOR = {E. Ohlebusch},
TITLE = {Termination of Logic Programs: Transformational Methods Revisited},
JOURNAL = {Applicable Algebra in Engineering, Communication and Computation},
VOLUME = {12},
NUMBER = {1--2},
PAGES = {73--116},
YEAR = {2001},
PUBLISHER = {Springer},
ADDRESS = {Heidelberg},
</bibtex>

[[Category:Bibtex]]
[[Category:BibtexNews]]

Bibtex:Ohlebusch01

2008-03-29T21:10:15Z

Nowonder: New page: <bibtex>  @article{Ohlebusch01, AUTHOR = {E. Ohlebusch}, TITLE = {Termination of Logic Programs: Transformational Methods ...

<bibtex>

@article{Ohlebusch01,
AUTHOR = {E. Ohlebusch},
TITLE = {Termination of Logic Programs: Transformational Methods Revisited},
JOURNAL = {Applicable Algebra in Engineering, Communication and Computation},
IN = {svdlcjklnds},
VOLUME = {12},
NUMBER = {1--2},
PAGES = {73--116},
YEAR = {2001},
PUBLISHER = {Springer},
ADDRESS = {Heidelberg},
</bibtex>

[[Category:Bibtex]]
[[Category:BibtexNews]]

Bibtex:SGST06

2008-03-29T20:59:15Z

Nowonder:

<bibtex>

@inproceedings{LOPSTR06,
AUTHOR = {P. Schneider-Kamp and J. Giesl and A. Serebrenik and R. Thiemann},
TITLE = {Automated Termination Analysis for Logic Programs by Term Rewriting},
BOOKTITLE = {LOPSTR~'06},
YEAR = {2007},
SERIES = {Lecture Note in Computer Science},
VOLUME = {4407},
PAGES = {177--193},
PUBLISHER = {Springer},
ADDRESS = {Heidelberg}
}
</bibtex>

[[Category:Bibtex]]
[[Category:BibtexNews]]

Bibtex:SGST06

2008-03-29T20:55:32Z

Nowonder:

<bibtex>

@inproceedings{LOPSTR06,
AUTHOR = {P. Schneider-Kamp and J. Giesl and A. Serebrenik and R. Thiemann},
TITLE = {{Automated Termination Analysis for Logic Programs by Term Rewriting}},
BOOKTITLE = {LOPSTR~'06},
YEAR = {2007},
SERIES = lncs,
VOLUME = {4407},
PAGES = {177--193},
PUBLISHER = {Springer},
ADDRESS = {Heidelberg}
}
</bibtex>

[[Category:Bibtex]]
[[Category:BibtexNews]]

Termination Portal

2008-03-29T20:54:29Z

Nowonder: /* Welcome */

Termination is a fundamental topic in computer science. While classical results state the undecidability of various termination problems, automated methods have successfully been developed that prove termination or non-termination in practical cases.
Research in termination analysis offers many challenges both in theory (mathematical logic, proof theory) and practice (software development, formal methods).

This portal aims to provide the research community with up-to-date information about the field
of termination analysis.
The main sections are [[:Category:People|People]] (information about researchers in termination analysis),
[[:Category:News|News]] (information about events and new publications),
[[:Category:Tools|Tools]] (information about tools for automated termination analysis), and
[[:Category:References|References]] (publications related to termination analysis).
Additionally, the portal provide information about past and future [[WST|workshops]] and [[Termination Competition|competitions]].

=Recent News=
<dpl>
category=News
shownamespace=false
count=10
ordermethod=lastedit
order=descending
includepage={News}:date:text
format =,,\n,
table =class="wikitable",Caption,Date,Text
tablerow =|%%
</dpl>

=New Publications=
<dpl>
category=BibtexNews
shownamespace=false
count=10
ordermethod=lastedit
order=descending
includepage=%0[100]
format =,,\n,
table =class="wikitable",Name,Content
tablerow =|%%
</dpl>

News:Termination Portal Online

2008-03-29T20:53:25Z

Nowonder:

Template:AddNews

2008-03-29T20:53:11Z

Nowonder:

News:Termination Portal Online

2008-03-29T20:49:20Z

People:Peter Schneider-Kamp

2008-03-29T18:29:45Z

Nowonder:

{{Person
|firstname=Peter
|middlenames=
|lastname=Schneider-Kamp
|titles=
|email=psk@informatik.rwth-aachen.de
|homepage=http://schneider-kamp.de
|country=Germany
|university=RWTH Aachen
|department=Research Group Computer Science 2
|role=Research and Teaching Assistant 
}}



http://verify.rwth-aachen.de/psk/psk.jpg

People:Peter Schneider-Kamp

2008-03-29T18:28:30Z

Nowonder:

{{Person
|firstname=Peter
|middlenames=
|lastname=Schneider-Kamp
|titles=
|email=psk@informatik.rwth-aachen.de
|homepage=http://schneider-kamp.de
|country=Germany
|university=RWTH Aachen
|department=Research Group Computer Science 2
|role=Research and Teaching Assistant 
}}



http://verify.rwth-aachen.de/psk/pskfull.jpg

People:René Thiemann

2008-03-29T17:49:19Z

Nowonder:

{{Person
|firstname=René
|middlenames=
|lastname=Thiemann
|titles=
|email=rene.thiemann@uibk.ac.at
|homepage=http://cl-informatik.uibk.ac.at/~thiemann/
|country=Austria
|university=University of Innsbruck
|department=Computational Logic Group
|role=Research Assitent 
}}