2020
9th Confluence Competition
Aart Middeldorp

Kiraku Shintani

Naoki Nishida

Johannes Waldmann

http://project-coco.uibk.ac.at/2020

Outline

1. Acknowledgements
2. History
3. 2020

IWC 2020

June 30

CoCo Live View

1. Acknowledgements

2/29

Acknowledgements• CoCo 2020 tool authors

IWC 2020

June 30

CoCo Live View

1. Acknowledgements

3/29

Acknowledgements• CoCo 2020 tool authors• Fabian Mitterwallner

IWC 2020

June 30

CoCo Live View

1. Acknowledgements

3/29

Acknowledgements• CoCo 2020 tool authors• Fabian Mitterwallner• IWC 2020 chairs

IWC 2020

June 30

CoCo Live View

1. Acknowledgements

3/29

Acknowledgements• CoCo 2020 tool authors• Fabian Mitterwallner• IWC 2020 chairs• CoCo 2020 panel• Frédéric Blanqui• Cynthia Kop• Geoff Sutcliffe

IWC 2020

June 30

CoCo Live View

1. Acknowledgements

3/29

Outline

1. Acknowledgements
2. History
3. 2020

IWC 2020

June 30

CoCo Live View

2. History

4/29

2012

TRS CPFACPCSI
Saigawa
CeTA

IWC 2020

June 30

CoCo Live View

2. History

5/29

2013

TRS CPFACPCSI
Saigawa
CeTA

IWC 2020

June 30

CoCo Live View

2. History

5/29

2014

TRS CPF CTRS

ACP
CSI
Saigawa
CeTA
CoLL
ConConCO3

IWC 2020

June 30

CoCo Live View

2. History

5/29

2015

TRS CPF CTRS HRS GCR NRS

ACP
CSI
CeTA
CoLL-Saigawa
ConConCO3
CoScartACPH
CSIˆhoAGCP
NoCo

IWC 2020

June 30

CoCo Live View

2. History

5/29

2016

TRS CPF CTRS HRS GCR NRS UN

CPF-CTRS

ACP
CSI
CeTA
CoLL-Saigawa
ConConCO3
CoScartACPH
CSIˆho
AGCP
Nrbox
FORT

IWC 2020

June 30

CoCo Live View

2. History

5/29

2017

TRS CPF CTRS HRS GCR NFP UNR CPF-CTRS UNC

ACP
CSI
CeTA
CoLL-Saigawa
ConConCO3
ACPH
CSIˆho
AGCP
FORT
SOL

IWC 2020

June 30

CoCo Live View

2. History

5/29

2018

TRS CPF CTRS HRS GCR NFP UNR CPF-CTRS UNC

ACP
CSI
CeTA
CoLL-Saigawa
ConConCO3

CSIˆho
AGCP
FORT
SOL

IWC 2020

June 30

CoCo Live View

2. History

5/29

2019

TRS CPF CTRS HRS GCR NFP UNR CPF-CTRS UNC COM INF SRS

ACP
CSI
CoLL
CeTA
CoLL-Saigawa
ConConCO3
infChecker
maedmax
CSIˆho
AGCP
Moca
FORT
noko-leipzig
non-reach
IWC 2020

June 30

CoCo Live View

2. History

5/29

• CoCo is powered by StarExec

IWC 2020

June 30

CoCo Live View

2. History

6/29

• CoCo is powered by StarExec• exciting to watch

IWC 2020

June 30

CoCo Live View

2. History

6/29

• CoCo is powered by StarExec• exciting to watch, partly due to real-time yes / no conflicts

IWC 2020

June 30

CoCo Live View

2. History

6/29

final slide CoCo 2019 presentation• CoCo 2020 most likely in Paris, collocated with FSCD / IJCAR• separate YES and NO results=⇒

more winners• new T-shirt for participating tool authors

IWC 2020

June 30

CoCo Live View

2. History

7/29

final slide CoCo 2019 presentation• CoCo 2020 most likely in Paris, collocated with FSCD / IJCAR• separate YES and NO results=⇒

more winners• new T-shirt for participating tool authors

IWC 2020

June 30

CoCo Live View

2. History

7/29

IWC 2020

June 30

CoCo Live View

2. History

8/29

IWC 2020

June 30

CoCo Live View

2. History

8/29

Outline

1. Acknowledgements
2. History
3. 2020
Categories

IWC 2020

June 30

Rules

CoCo Live View

Live View

3. 2020

Categories

Results

9/29

Categories
TRS

confluence of first-order term rewrite systems

CPF

certification for TRS

CTRS

confluence of first-order conditional term rewrite systems

HRS

confluence of higher-order rewrite systems

GCR

ground-confluence of many-sorted first-order rewrite systems

CPF-CTRS

certification for CTRS

NFP

normal form property of first-order rewrite systems

UNR

unique normal forms wrt reduction of first-order rewrite systems

UNC

unique normal forms wrt conversion of first-order rewrite systems

COM

commutation of first-order rewrite systems

INF

infeasibility

SRS

confluence of string rewrite systems

IWC 2020

June 30

CoCo Live View

3. 2020

Categories

10/29

2019

TRS CPF CTRS HRS GCR NFP UNR CPF-CTRS UNC COM INF SRS

ACP
CSI
CoLL
CeTA
CoLL-Saigawa
ConConCO3
infChecker
maedmax
CSIˆho
AGCP
Moca
FORT
noko-leipzig
non-reach
IWC 2020

June 30

CoCo Live View

3. 2020

Categories

11/29

2020

TRS CPF CTRS HRS GCR NFP UNR CPF-CTRS UNC COM INF SRS

ACP
CSI
CoLL
CeTA
CoLL-Saigawa
ConConCO3
infChecker
CSIˆho
AGCP
Moca
FORT-hSOL
non-reach
IWC 2020

June 30

CoCo Live View

3. 2020

Categories

11/29

Outline

1. Acknowledgements
2. History
3. 2020
Categories

IWC 2020

June 30

Rules

CoCo Live View

Live View

3. 2020

Rules

Results

12/29

Competition Rules• Scoring• 100 random problems per category, using seed digits provided by panel members• tools output YES or NO or MAYBE on first line followed by proof• separate rankings for YES and NO and combined YES / NO answers• winning tools of 2019 participate as demonstration tools in 2020

IWC 2020

June 30

CoCo Live View

3. 2020

Rules

13/29

Competition Rules• Scoring• 100 random problems per category, using seed digits provided by panel members• tools output YES or NO or MAYBE on first line followed by proof• separate rankings for YES and NO and combined YES / NO answers• winning tools of 2019 participate as demonstration tools in 2020

• Secret Problems• guaranteed to be selected• at most two problems per category per tool
• 4 secret problems submitted

IWC 2020

June 30

CoCo Live View

3. 2020

Rules

13/29

Competition Rules• Scoring• 100 random problems per category, using seed digits provided by panel members• tools output YES or NO or MAYBE on first line followed by proof• separate rankings for YES and NO and combined YES / NO answers• winning tools of 2019 participate as demonstration tools in 2020

• Secret Problems• guaranteed to be selected• at most two problems per category per tool
• 4 secret problems submitted, including a(b(a(x))) → a(a(b(a(b(x)))))

IWC 2020

June 30

CoCo Live View

3. 2020

Rules

13/29

Competition Rules• Scoring• 100 random problems per category, using seed digits provided by panel members• tools output YES or NO or MAYBE on first line followed by proof• separate rankings for YES and NO and combined YES / NO answers• winning tools of 2019 participate as demonstration tools in 2020

• Secret Problems• guaranteed to be selected• at most two problems per category per tool
• 4 secret problems submitted, including a(b(a(x))) → a(a(b(a(b(x)))))• Incorrect Results• tools with incorrect results (observed during live competition due to YES / NO conflict,or communicated afterwards by tool authors to SC) are excluded from results table
IWC 2020

June 30

CoCo Live View

3. 2020

Rules

13/29

• (corrected) tools are available from CoCoWeb for testing

IWC 2020

June 30

CoCo Live View

3. 2020

Rules

14/29

• (corrected) tools are available from CoCoWeb for testing

IWC 2020

June 30

CoCo Live View

3. 2020

Rules

14/29

• (corrected) tools are available from CoCoWeb for testing• confluence problems database (COPS) consists of 1150 problems

IWC 2020

June 30

CoCo Live View

3. 2020

Rules

14/29

CoCo 2020 Live View

http://cocograph.uibk.ac.at/2020.html

IWC 2020

June 30

CoCo Live View

3. 2020

Live View

15/29

Outline

1. Acknowledgements
2. History
3. 2020
Categories

IWC 2020

June 30

Rules

CoCo Live View

Live View

3. 2020

Results

Results

16/29

2019 results

ACP
CSI
TRS category• ACP breaks 3-year hegemony of CSI• incorrect answers by CoLL-Saigawa

IWC 2020

June 30

CoCo Live View

3. 2020

Results

17/29

ACP (Automated Confluence Prover)
Takahito Aoto
• Entered to TRS/CPF-TRS/UNC/CTRS/COM/SRS• Written in Standard ML of New Jersey (SML/NJ)• Version: 0.10 (2009) · · · 0.70 (2019)• Implementing multiple direct methods and divide-andconquer methods• For UNC, we use a decision procedure for shallow TRSs,
based on:A Fast Decision Procedure for UNC of Shallow TRS,
M. Yamaguchi and T. Aoto, FSCD 2020
We couldn’t make any efforts on ACP this year.

CoLL-Saigawa v1.5 (Shintani & Hirokawa, JAIST)

LL

CoLL
YES/NOTRS

CoLL-Saigawa

1/2

CoLL-Saigawa v1.5 (Shintani & Hirokawa, JAIST)

LL

CoLL
YES/NO

TRS
non-LLCoLL-Saigawa

Saigawa

1/2

CoLL-Saigawa v1.5 (Shintani & Hirokawa, JAIST)

LL

CoLL
YES/NO

TRS
non-LL

Saigawa

CoLL-Saigawa uses MiniSmt, NaTT, and Z3

CoLL-Saigawa

1/2

CoLL-Saigawa v1.5 (Shintani & Hirokawa, JAIST)

LL

CoLL
YES/NO

TRS
non-LL

Saigawa

CoLL-Saigawa uses MiniSmt, NaTT, and Z3
it no longer uses TTT2 (= CSI)
CoLL-Saigawa

1/2

New Features

CoLL-Saigawa

2/2

New Features
improved performance of AC-related methods

CoLL-Saigawa

2/2

New Features
improved performance of AC-related methods
supported upside-parallel/outside closedness

CoLL-Saigawa

2/2

New Features
improved performance of AC-related methods
supported upside-parallel/outside closedness
Theorem (Oyamaguchi and Ohta 1997)

left-linear TRS is confluent if
p



Mp





>

Mp

Q



q ∪→
←
−o→
− ⊆ ←
−
− = for all p >  and




q ∪→
q ∪→
←
−o→
− ⊆ (←−− ) · (←−−)

q t if s −q t for some Q ⊆ {q | |q| 6 |p|}where, s −→→CoLL-Saigawa

2/2

New Features
improved performance of AC-related methods
supported upside-parallel/outside closedness
Theorem (Oyamaguchi and Ohta 2004)

left-linear TRS is confluent if
p



≯p







>



←
−o→
− ⊆ ←− ∪ →− = for all p > 

and



q ∪→
q ∪→
←
−o→
− ⊆ (←−− ) · (←−−)

CoLL-Saigawa

2/2

New Features
improved performance of AC-related methods
supported upside-parallel/outside closedness
supported criteria based on parallel/simultaneous critical pairs

CoLL-Saigawa

2/2

New Features
improved performance of AC-related methods
supported upside-parallel/outside closedness
supported criteria based on parallel/simultaneous critical pairs
Theorem (Toyama 1981)

left-linear TRS is confluent if


·

·

||

P
·



||

∗

s

t

u
||

·

∗

Q

v

for some v with Var(v, Q) ⊆ Var(s, P )CoLL-Saigawa

2/2

New Features
improved performance of AC-related methods
supported upside-parallel/outside closedness
supported criteria based on parallel/simultaneous critical pairs
Theorem (Toyama 1981)

Theorem (Okui 1998)

left-linear TRS is confluent if

left-linear TRS is confluent if



·

·

||

P
·



||

∗

s

t

∗

·

u
||

·

Q
·

v

for some v with Var(v, Q) ⊆ Var(s, P )CoLL-Saigawa

2/2

·
∗

·

CoCo 2020 Participant:Fabian Mitterwallner

CSI 1.2.4

Aart Middeldorp

[Google Maps]

CSI 1.2.4

CoCo 2020

30 June 2020

2/3

[Google Maps]C

CSI 1.2.4

CoCo 2020

30 June 2020

2/3

[Google Maps]

CS

CSI 1.2.4

CoCo 2020

30 June 2020

2/3

[Google Maps]

CSI

CSI 1.2.4

CoCo 2020

30 June 2020

2/3

[Google Maps]C S I 1.2.4

CSI 1.2.4

CoCo 2020

30 June 2020

2/3

• open source• convenient web interface• http://cl-informatik.uibk.ac.at/software/csi/

CSI 1.2.4

CoCo 2020

30 June 2020

3/3

• open source• convenient web interface• http://cl-informatik.uibk.ac.at/software/csi/
CoCo 2019 Categories• CPF-TRS

NFP

CSI 1.2.4

CoCo 2020

TRS

UNC

30 June 2020

UNR

SRS

3/3

• open source• convenient web interface• http://cl-informatik.uibk.ac.at/software/csi/
CoCo 2019 Categories• CPF-TRS

NFP

CSI 1.2.4

CoCo 2020

TRS

UNC

30 June 2020

UNR

SRS

1st place3/3• open source• convenient web interface• http://cl-informatik.uibk.ac.at/software/csi/
CoCo 2020 Categories• CPF-TRS

NFP

CSI 1.2.4

CoCo 2020

TRS

UNC

30 June 2020

UNR

SRS

3/3

• open source• convenient web interface• http://cl-informatik.uibk.ac.at/software/csi/
CoCo 2020 Categories• CPF-TRS

NFP

TRS

UNC

UNR

SRS

New Features• criterion for confluence of upside-parallel-closed rewrite systems(Oyamaguchi and Ohta, RTA 1997)

CSI 1.2.4

CoCo 2020

30 June 2020

3/3

• open source• convenient web interface• http://cl-informatik.uibk.ac.at/software/csi/
CoCo 2020 Categories• CPF-TRS

NFP

TRS

UNC

UNR

SRS

New Features• criterion for confluence of upside-parallel-closed rewrite systems(Oyamaguchi and Ohta, RTA 1997)• minor changes to the strategy for (certified) confluence for performance improvements

CSI 1.2.4

CoCo 2020

30 June 2020

3/3

2019 results

CSI+CeTA
ACP+CeTA
CPF-TRS category

IWC 2020

June 30

CoCo Live View

3. 2020

Results

18/29

CoCo 2020 Participant: CeTA 2.39
Jonas Schöpf, Christian Sternagel,
René Thiemann and Akihisa Yamada

CeTA 2.39

• CeTA: certifier of confluence proofs, verified in Isabelle/HOL• several confluence techniques supported, see a complete list at:

http://cl-informatik.uibk.ac.at/software/ceta/• no new confluence techniques in CeTA 2.39
• improved support for confluence techniques based on (relative) termination• added support for weighted path order (WPO)• added support for max-polynomial interpretations, with WPO or stand-alone• certifiable proofs available via TTT2 and, for the first time, via NaTT

• new potential to optimise your certified confluence strategy

CoCo 2020 Participant: CeTA 2.39

IWC

June 30, 2020

1/1

2019 results

ACP

CTRS category• surprise win by ACP• incorrect answers by ConCon and CO3

IWC 2020

June 30

CoCo Live View

3. 2020

Results

19/29

CO3

(Ver. 2.1)
a COnverter for proving COnfluence of COnditional TRSs

Naoki Nishida
Nagoya University, Japan

Overview
CO3 proves confluence of 3-DCTRSs or infeasibility of conditions by using
very simple termination/confluence criteria for TRSs,
the improved sequential unraveling Uconf [Gmeiner et al, 13], andnarrowing trees [Nishida & Maeda, 18]

Infeasibility Criterion for Condition c w.r.t. DCTRSs
Uconf (R) is right-linear and a narrowing tree for c defines ∅ [Maeda et al, 19]

Confluence Criteria for syntactically deterministic 3-CTRSs R
R is weakly-left-linear and Uconf (R) is confluent [Gmeiner et al, 13], or

Uconf (R) is terminating and right-linearand ∀hs, ti ⇐ c ∈ CP(R), (c =  ∧ s = t) ∨ “c is infeasible” [Maeda et al, 19]

Christian Sternagel

ConCon 1.10
inlining of conditions
removal of infeasible rules
A

B

C

N

U

infeasibility

TTT2

DVT

ConCon 1.10

MædMax

9th IWC – 30 June 2020

nonreach

CSI

1/2• open source• http://cl-informatik.uibk.ac.at/software/concon/
New Features• external infeasibility tool: nonreach by Florian Meßner
CoCo 2020 Categories• CTRS• CPF-CTRS
• INF

DVT

ConCon 1.10

9th IWC – 30 June 2020

2/2

2019 results

CSIˆhoHRS category• more participation welcome!

IWC 2020

June 30

CoCo Live View

3. 2020

Results

20/29

Julian Nagele[Google Maps]

CSI

Julian Nagele[Google Maps]C S I ˆ h o 0.3.2

Julian Nagele[Google Maps]C S I ˆ h o 0.3.2• extension of CSI for higher-order (pattern) rewrite systems• http://cl-informatik.uibk.ac.at/software/csi/ho/

2020• no new features

1

The System SOL version 2020
B Haskell-based tool for analysing conﬂuence and termination
B Authors: Makoto Hamana (Main developer, Gunma University)
Kentaro Kikuchi (Tohoku University)
Date Yao Faustin Dieudonne, Kazuki Fuju (Gunma University)
B References:– Polymorphic computation systems: Theory and practice of conﬂuence withcall-by-value, Hamana. Science of Computer Programming, Vo.187, 2020.
– How to prove decidability of equational theories with second-order computation
analyser SOL, Hamana, Abe, Kikuchi. Journal of Functional Programming, Vol. 29,
e20, 2019.

B CR: Knuth and Bendix’s critical pair checking
using Functions-as-Constructors uniﬁcation (FCU) [Libal,Miller’16]
B SN: - the General Schema criterion [Blanqui, RTA’00,TCS’16]- Modular termination of second-order computation systems
B Contact Hamana (hamana@gunma-u.ac.jp)
if you are interested in/want to use SOL

2019 results

ACP
FORT
GCR category• only previously unsolved problems due to incorrect selection query

IWC 2020

June 30

CoCo Live View

3. 2020

Results

21/29

AGCP (Automated Ground Confluence Prover)
Takahito Aoto
A ground confluence prover for many-sorted TRSs
• An entrant of GCR category• Written in Standard ML of New Jersey (SML/NJ)• Methods:− rewriting induction for bounded convertibility− equivalent transformations, disproving methods• Based on:
Improvements of the Rewriting Induction Approachfor proving GCR, Aoto/Toyama/Kimura, FSCD 2017
We couldn’t make any efforts on AGCP this year.

2019 results

CSI
FORT
NFP category

IWC 2020

June 30

CoCo Live View

3. 2020

Results

22/29

2019 results

CSI
FORT
UNR category

IWC 2020

June 30

CoCo Live View

3. 2020

Results

23/29

2019 results

ConCon+CeTA

CPF-CTRS category

IWC 2020

June 30

CoCo Live View

3. 2020

Results

24/29

2019 results

ACP
CSI

FORT
UNC category

IWC 2020

June 30

CoCo Live View

3. 2020

Results

25/29

2019 results

FORT

COM category• first ever win for FORT in any category• incorrect answers by ACP and CoLL

IWC 2020

June 30

CoCo Live View

3. 2020

Results

26/29

CoLL: Commutation Tool for Left-Linear TRSs{(R, S)}CoLL

YES/NOauthor: Kiraku Shintani (JAIST)
version: 1.5
code: OCaml (6000 LoC)MAYBE

CoLL: Commutation Tool for Left-Linear TRSs{(R, S)}- Knuth-Bendix- AC theory- closedness criteria- rule labeling

YES/NOMAYBE?

MAYBE

CoLL: Commutation Tool for Left-Linear TRSs{(R, S)}- Knuth-Bendix- AC theory- closedness criteria- rule labeling

YES/NO

MAYBE{Ri }I × {Sj }Jfind commuting subsystems

∅

MAYBE

- basedcommutation lemma:
S on Hindley’s
S
R
and
S
i
i
j j commute if Ri and Sj commute for all i, j
CoLL

1/2

CoLL: Commutation Tool for Left-Linear TRSs{(R, S)}- Knuth-Bendix- AC theory- closedness criteria- rule labeling

YES/NO

MAYBE{Ri }I × {Sj }Jfind commuting subsystems

∅

MAYBE

- basedcommutation lemma:
S on Hindley’s
S
R
and
S
i
i
j j commute if Ri and Sj commute for all i, j
- left-linearity is often essential for commutation

CoLL

1/2

What’s new?

supported several closedness criteria
1 commutation
almost parallel closedness (Toyama 1988)2

self commutation (confluence)extension of parallel closedness (Toyama 1981)
simultaneous closedness (Okui 1998)
upside parallel closedness (Ohta and Oyamaguchi 1997)
outside closedness (Ohta and Oyamaguchi 2003)

and also improved AC-related feature

CoLL

2/2

supported by

CoCo 2020 Participant:Fabian Mitterwallner

Aart Middeldorp

project P30301

FORT-h 0.9
Bertram Felgenhauer

FORT-h

FORT-h 0.9

CoCo 2020

30 June 2020

2/3

FORT-hpropertyTRS

yes | no | ?

FORT-h 0.9

CoCo 2020

30 June 2020

2/3

FORT-hlinear variable-separated
propertyTRS∀ s ∃ t (s →∗ t ∧ ¬ ∃ u (t → u)k v ∨ v →=⇒ ∃ v (s −→− t))yes | no | ?
property is arbitrary formula in first-order theory of rewriting

FORT-h 0.9

CoCo 2020

30 June 2020

2/3

CoCo 2019 Categories (FORT)
GCR

NFP

FORT-h 0.9

UNC

CoCo 2020

UNR

30 June 2020

COM

3/3

CoCo 2019 Categories (FORT)
GCR

NFP

FORT-h 0.9

UNC

CoCo 2020

UNR

30 June 2020

COM

1st place

3/3

CoCo 2020 Categories (FORT-h)
GCR

NFP

FORT-h 0.9

UNC

CoCo 2020

UNR

30 June 2020

COM

3/3

CoCo 2020 Categories (FORT-h)
GCR

NFP

UNC

UNR

COM

Differences FORT and FORT-h• modified decision procedure

FORT-h 0.9

CoCo 2020

30 June 2020

3/3

CoCo 2020 Categories (FORT-h)
GCR

NFP

UNC

UNR

COM

Differences FORT and FORT-h• modified decision procedure• supports linear variable-separated TRSs

FORT-h 0.9

CoCo 2020

30 June 2020

3/3

CoCo 2020 Categories (FORT-h)
GCR

NFP

UNC

UNR

COM

Differences FORT and FORT-h• modified decision procedure• supports linear variable-separated TRSs
• more expressive theory (→> )FORT-h 0.9

CoCo 2020

30 June 2020

3/3

CoCo 2020 Categories (FORT-h)
GCR

NFP

UNC

UNR

COM

Differences FORT and FORT-h• modified decision procedure• supports linear variable-separated TRSs
• more expressive theory (→> )• goal: certified results

FORT-h 0.9

CoCo 2020

30 June 2020

3/3

CoCo 2020 Categories (FORT-h)
GCR

NFP

UNC

UNR

COM

Differences FORT and FORT-h• modified decision procedure• supports linear variable-separated TRSs
• more expressive theory (→> )• goal: certified results

http://cl-informatik.uibk.ac.at/software/FORT/

FORT-h 0.9

CoCo 2020

30 June 2020

3/3

2019 results

infChecker
non-reach

Moca
INF category• most contested category with 6 participating tools• incorrect answers by ConCon• infChecker is only tool with NO answers

IWC 2020

June 30

CoCo Live View

3. 2020

Results

27/29

infChecker at CoCo 2020

Raúl Gutiérrez1

Salvador Lucas2

PARIS , J UNE 30, 2020
1 Universidad Politécnica de Madrid

Spain
2 Valencian Research Institute for Artificial Intelligence

Universitat Politècnica de València
Spain

Description• infChecker is a tool for checking (in)feasibility of goalsni
G = {Fi }mi=1 , where Fi = (sij ./ij tij )i=1 .

• ./ij represents predicates on terms defined by provabilityof goals s ./ij t with respect to a first-order theories Th./ij .

• ./ij can be one of the following predicates:• One (CS-)rewriting step (->, \->).
• Zero or more (CS-)rewriting steps (->*, \->*).
• One or more (CS-)rewriting steps (->+, \->+).
• Subterm (|>=) and strict subterm (|>).
• (CS-)Joinability (->*<-, \->*<-/).
• One (CS-)convertibility step (<-->, <-/\->).
• Zero or more (CS-)convertibility steps (<-->*, <-/\->*).
1/3

Implementation• The tool is available here:

http://zenon.dsic.upv.es/infChecker/.
• It is written in Haskell and provides a first implementationof the Feasibility Framework, where four processors
have been implemented:• PSat integrates a satisfiability approach to proveinfeasibility using model generators as AGES andMace4 to find a proof.
• PUR simplifies problems by removing non-usable rules.
• PProv integrates a logic-based approach to program
analysis to prove feasibility by theorem proving. In
infChecker, we use the theorem prover Prover9.
• PNC adapt the processor that narrow conditions in the 2D
DP framework for proving operational termination of CTRs
to be used with feasibility sequences.
2/3

Strategy and Results• Our proof strategy is:
1
2
3
4
5

we apply PUR whenever it is sound and complete;
we try to prove feasibility using PProv ;if PProv fails, we apply PSat ;if PSat fails, we apply PNC ;if PNC succeeds and modifies the feasibility sequence, we
repeat the strategy, otherwise we return MAYBE.

• Bibliography:
GL20 R. Gutiérez and S. Lucas. Automatically Proving and Disproving
Feasibility Conditions. In Proc. of IJCAR’2020, LNCS
12167:416–435. Springer, 2020.
Luc19 S. Lucas. Proving semantic properties as first-order satisfiability.
Artificial Intelligence 277, paper 103174, 24 pages, 2019.
LG18 S. Lucas and R. Gutiérrez. Use of Logical Models for Proving
Infeasibility in Term Rewriting. Information Processing Letters,
136:90-95, 2018.

3/3

Theorem Prover Moca 0.2 (Oi and Hirokawa, JAIST)
Infeasibility Problem:

_
i



si σ →−
6 R ti σ for every σ?
∗

Theorem Prover Moca 0.2 (Oi and Hirokawa, JAIST)
Infeasibility Problem:

_
i



si σ →−
6 R ti σ for every σ?
∗transformation

Horn Satisfiability Problem: M |= Φ for some M?

Theorem Prover Moca 0.2 (Oi and Hirokawa, JAIST)
Infeasibility Problem:

_
i



si σ →−
6 R ti σ for every σ?
∗transformation

Horn Satisfiability Problem: M |= Φ for some M?
transformation

Word Problem: T ≈6 E F?

Theorem Prover Moca 0.2 (Oi and Hirokawa, JAIST)
Infeasibility Problem:

_
i



si σ →−
6 R ti σ for every σ?
∗transformation

Horn Satisfiability Problem: M |= Φ for some M?
transformation

Word Problem: T ≈6 E F?
Maximal Ordered Completion
with Approximation

YES / MAYBE
1/4

Transformations to Word Problem
Infeasibility Problem

CTRS:
x−0→x
0−x→0
s(x) − s(y) → x − yCondition:∗x−x→− R s(x)Transformations to Word Problem
Infeasibility Problem

Horn Satisfiability Problem

CTRS:
x−0→x
0−x→0
s(x) − s(y) → x − yFormulas:
∀x.
x−0=x
∀x.
0−x=0
∀x, y. s(x) − s(y) = x − y∀x.
x − x 6= s(x)Condition:∗x−x→− R s(x)Transformations to Word Problem
Infeasibility Problem

Horn Satisfiability Problem

CTRS:
x−0→x
0−x→0
s(x) − s(y) → x − yFormulas:
∀x.
x−0=x
∀x.
0−x=0
∀x, y. s(x) − s(y) = x − y∀x.
x − x 6= s(x)Condition:∗x−x→− R s(x)Word Problem

ES:

x−0=x
0−x=0
s(x) − s(y) = x − yf(x − x, x) = T
f(s(x), x) = F
Goal:

2/4

T=F

Transformations to Word Problem
Infeasibility Problem

Horn Satisfiability Problem

CTRS:
x−0→x
0−x→0
s(x) − s(y) → x − yFormulas:
∀x.
x−0=x
∀x.
0−x=0
∀x, y. s(x) − s(y) = x − y∀x.
x − x 6= s(x)Condition:∗x−x→− R s(x)Infeasible

Word Problem

ES:

x−0=x
0−x=0
s(x) − s(y) = x − yf(x − x, x) = T
f(s(x), x) = F
Goal:

⇐=

Satisfiable
2/4

⇐=

T=F

T≈
6 EF

Approximation for Showing T ≈
6 EF
Fact

if ≈E ⊆ ≈E 0 (E is approximated as E 0 ) then T ≈6 E 0 F implies T ≈
6 EF

3/4

Approximation for Showing T ≈
6 EF
Fact

if ≈E ⊆ ≈E 0 (E is approximated as E 0 ) then T ≈6 E 0 F implies T ≈6 EF
Original System E

x−0=x
0−x=0
s(x) − s(y) = x − yf(x − x, x) = T
f(s(x), x) = F

admits no complete TRS
3/4

Approximation for Showing T ≈
6 EF
Fact

if ≈E ⊆ ≈E 0 (E is approximated as E 0 ) then T ≈6 E 0 F implies T ≈6 EF
Original System E

Approximation E 0

admits no complete TRS

admits complete TRS!

x−0=x
0−x=0
s(x) − s(y) = x − yf(x − x, x) = T
f(s(x), x) = F

x−0=x
0−x=0
s(x) − s(y) = x − yf(x − x, y) = T
f(s(x), x) = F

3/4

New Features

Moca version 0.2 supports:(Oi 2019)

generalized split-if encoding
inlining for conditional rewrite rules

4/4(Sternagel & Sternagel 2017)

Florian Meßner

nonreachrule inlining
preprocessing
inductive rule analysis

problem decomposition

narrowing non-root reachability

nonreach

30 June 2020

fast checks

etcap

inductive stg

1/2• open source• https://bitbucket.org/fmessner/nonreach/Features• implements fast infeasibility checks based on tcap and the inductive symboltransition graph• combined with decomposition into easier subproblems• easy interface• Yes and No results• can output certificates
CoCo 2020 Category• INF
nonreach

30 June 2020

2/2

2019 results

CSI

noko-leipzig

ACP
SRS category• noko-leipzig produces most NO answers

IWC 2020

June 30

CoCo Live View

3. 2020

Results

28/29

and the 2020 winners are . . .

http://cocograph.uibk.ac.at/2020.html

IWC 2020

June 30

CoCo Live View

3. 2020

Results

29/29