left

PROLOG

right
AProVE Help SystemUser InterfaceGraphical User InterfaceSelecting OptionsUser DefinedPROLOG

The Prolog user defined options panel offers you the possibility to control the details of termination proving for Prolog programs. Therefore it provides you with 3 different configuration boxes . prologstrategy

The query configuration box (1)

After loading a Prolog file, AProVE will collect all the queries mentioned in the file as either normal Prolog queries or query mode lines and will display their types in this configuration box. The user may now chose to add new query types or delete existing ones.

When the user starts the proof by pressing the Go button the query types listed in this box will determine the moding during the transformation.

Furthermore, all clauses that are neither directly nor indirectly needed to answer at least one of the listed query types will be ignored entirely if the unrequested clause remover is included in the transformation process.

The TRS and SCC configuration boxes (2 and 3)

The rest of the panel does not differ from the normal TRS configuration panel and controls the proving process once the Prolog program is transformed into a TRS.