PV1 ⊧ nonreachdetermines whether a problem for a rewrite system is nonreachable or infeasible

nonreach is an automated tool for nonreachability analysis that is intended as a drop-in addition to existing termination and confluence tools for term rewriting

Application domain/field

• Nonreachability analysis
• Reachability
• Termination

Type of tool

Nonreachability tool

Expected input

• Rewrite system
• Nonreachability or infeasibility problem

Format:

• Rewrite system: .trs file
• Problem: Defined as s -> t where s and t are terms. This should be given via one of the following options:
1. white-space-separated list of problems via command line or a file
2. infeasibility problem should be provided as part of the input rewrite system
3. Or given via standard input

Expected output

NO if nonreachability can be established for the problem. YES if it was given an infeasibility problem which is infeasible. MAYBE or TIMEOUT otherwise.

Internals

nonreach has been made to be a back end for reachability analysis tools.