FORT (2.0.1)

FORT is a decision and synthesis tool for the first-order theory of rewriting with respect to left-linear right-ground term rewrite systems.

Examples

Select example Example1 C21 C33 C34 C36 C38 C39 C40 C74 C80 C81 C82 C84 C111 C114 C115 C116 C212 C213 C214 C215 C223 C224 C225 C503 C505 C506 C507 C508 C509 C510 C511 C512 C543 C557 C647 C648 C649 C650 C651 C652 C653 C654 C655 C656 C657 C658 C659 C660 C661 C662 C663 C664 C665 C666 C667 C668 C669 C670 C671 C672 C673 C674 C675 C676 C677 C678 C679 C680 C681 C682 C683 C684 C685 C686 C687 C688 C689 C690 C691 C692 C693 C694 C695 C696 C697 C698 C699 C700 C701 C702 C703 C704 C705 C706 C707 C708 C709 C710 C711 C712 C713 C714 C715 C716 C717 C718 C719 C720 C721 C731 C732 C733 C734 C735 C736 C737 C738 C739 C740 C741 C761

Load own example

Syntax highlighting

Plain text TRS Synthesis

Tool input

(VAR) (RULES c1 -> c0 c1 -> c2 c2 -> g0(c1) c2 -> c3 c0 -> g0(c0) c3 -> g0(c3) )

Select Strategy

Decision tool

Formula

Synthesis tool