Procedura Ac4ft-Miner pracuje s akčními pravidly φ ∧ Φ ≈ ψ ∧ Ψ a s podmíněnými akčními pravidly φ ∧ Φ ≈ ψ ∧ Ψ /χ Zde φ, ψ, χ jsou booleovské atributy, φ je stabilní antecedent a ψ je stabilní sukcedent. Φ a Ψ jsou změny booleovských atributů, Φ je změna antecedentu a Ψ je změna sukcedentu. Symbol ≈ je Ac4ft-kvantifikátor. Zadání procedury se provádí v okně dle následujícího obrázku.

Zadává se množina relevantních akčních pravidel. Tlačítkem Validate se vyvolá kontrola zadání.

Tlačítkem Params je dostupný parametr Maximal number of hypotheses to be mined kterým se udává maximální počet nalezených pravidel. Po dosažení uvedeného maximálního počtu pravidel se běh procedury ukončí.

Tlačítkem Params jsou také dostupné parametry 'Strict action', a 'Sets overlaping', které jsou součástí definice množiny relevantních akčních pravidel.

Procedura se spustí jedním z tlačítek Run, Bkgrnd Run, Grid Run popsaných zde. Tlačítkem Show Results se zahajuje prohlížení a interpretace výsledků.

Tlačítkem Task Clone se provede vyklonování úlohy.

Ukázky aplikací procedury Ac4ft-Miner jsou zde.

Množina relevantních asociačních pravidel je dána

• zadáním množiny ANT_STAB relevantních stabilních antecedentů, to se zahajuje tlačítkem
  ANTECEDENT STABLE PART
• zadáním množiny SUCC_STAB relevantních sukcedentů, to se zahajuje tlačítkem
  SUCCEDENT STABLE PART
• zadáním množiny ANT_CHNG relevantních změn antecedentů, to se zahajuje tlačítkem
  ANTECEDENT VARIABLE PART
• zadáním množiny SUCC_CHNG relevantních změn antecedentů, to se zahajuje tlačítkem
  SUCCEDENT VARIABLE PART
• zadáním množiny COND relevantních podmínek, to se zahajuje tlačítkem CONDITION
• zadáním Acft-kvantifikátoru ∼, to se zahajuje tlačítkem QUANTIFIERS.

Množiny ANT_STAB, SUCC_STAB, ANT_CHNG, SUCC_CHNG a COND se zadávají jako množiny relevantních cedentů.

Alespoň jedna ze zadaných množin ANT_STAB a SUCC_STAB musí být neprázdná a zároveň alespoň jedna z množin ANT_CHNG a SUCC_CHNG musí být neprázdná.

Relevantní akční pravidla jsou akční pravidla φ ∧ Φ ≈ ψ ∧ Ψ taková, že

• φ ∈ ANT_STAB, Init(Φ) ∈ ANT_CHNG, Fin(Φ) ∈ ANT_CHNG,
• φ a Init(Φ) nemají společné atributy a ani φ a Fin(Φ) nemají společné atributy
• Init(Φ) a Fin(Φ) splňují podmínky dané parametrem 'Strict action'
• ψ ∈ SUCC_STAB, Init(Ψ) ∈ SUCC_CHNG, Fin(Ψ) ∈ SUCC_CHNG,
• ψ a Init(Ψ) nemají společné atributy a ani ψ a Fin(Ψ) nemají společné atributy
• Init(Ψ) a Fin(Ψ) splňují podmínky dané parametrem 'Strict action'
• φ a ψ nemají společné atributy

Relevantní akční pravidla jsou i podmíněná akční pravidla φ ∧ Φ ≈ ψ ∧ Ψ/χ taková, že

• φ ∧ Φ ≈ ψ ∧ Ψ je akční pravidlo
• φ , Init(Φ), Fin(Φ), ψ, Init(Ψ), Fin(Ψ) a χ nemají společné atributy.

Parametr Strict action se zadává volbami v rámci States Before and Action type v okně dle následujícího obrázku, které se vyvolá tlačítkem Params. .

Přednastavená volba States must be represented by the same sets of attributes which differ in coeficient (strict meaning of action) znamená, že booleovské atributy Init(Φ) a Fin(Φ) mají stejnou množinu atributů které se v nich vyskytují a nejméně u jednoho literálu se liší koeficient.

Druhá volba States may be represented by not related sets of attributes znamená, že se na atributy vyskytující se v booleovských atributech Init(Φ) a Fin(Φ) nekladou žádná omezení.

Parametr Sets overlaping se zadává volbami v rámci States Before and Action overlapping v okně dle následujícího obrázku, které se vyvolá tlačítkem Params. .

Přednastavená volba States must differ in all rows (i.e. overlapping states znamená, že podmatice dat M/(φ ∧ Init(Φ)) a M/(φ ∧ Fin(Φ)) nemají žádné společné řádky kde M je analyzovaná matice dat.

Druhá volba ''States must differ in at least one row (i.e. partially overlapping states allowed) znamená, že podmatice dat M/(φ ∧ Init(Φ)) a M/(φ ∧ Fin(Φ)) mohou mít společné řádky ale že existuje řádek, který patří jen do jedné z nich.

Kontrola zahrnuje jednak obecné kontroly společné pro všechny procedury a jednak kontroly zadání parametrů specifických pro Ac4ft-Miner.