left

CSR

right
AProVE Help SystemUser InterfaceGraphical User InterfaceSelecting OptionsUser DefinedCSR

For input type CSR (Context-Sensitive Rewriting) some special settings are available in user defined mode.

The Context-Sensitive strategy offers the selection of the strategy(1) the prover should show the termination for.

csrstrategy

If the Orthogonal checker(2) is active the prover checks whether CSR is orthogonal and in that case it switches to innermost termination.

The CSR to TRS Transformations are selectable with the Transformations combobox(3) and are added with add. Every transformation could only be added once. The prover could only be started with a non-empty list of transformations. Also the order of them are selectable with up   and down . delete   removes the selected transformation and delete   clears the list of transformations(4). If the prover is started for a CSR target the prover tries the first transformation if it succeeds it goes on with the technique selected in the TRS Configuration(6) and Scc Configuration. If parallel(5) is active the transformations are processed in parallel and the first proof is shown in the Result tab.