Answer Set Programming (ASP), a well-known declarative logic programming paradigm, has recently found practical application in Process Mining. In particular, ASP has been used to model tasks involving declarative specifications of business processes. In this area, Declare stands out as the most widely adopted declarative process modeling language, offering a means to model processes through sets of constraints valid traces must satisfy, that can be expressed in Linear Temporal Logic over Finite Traces (LTLf). Existing ASP-based solutions encode Declare constraints by modeling the corresponding LTLf formula or its equivalent automaton which can be obtained using established techniques. In this paper, we introduce a novel encoding for Declare constraints that directly models their semantics as ASP rules, eliminating the need for intermediate representations. We assess the effectiveness of this novel approach on two Process Mining tasks by comparing it with alternative ASP encodings and a Python library for Declare. Under consideration in Theory and Practice of Logic Programming (TPLP).

翻译：答案集编程（ASP）作为一种著名的声明式逻辑编程范式，最近在过程挖掘领域找到了实际应用。具体而言，ASP已被用于建模涉及业务流程声明式规范的任务。在该领域中，Declare作为最广泛采用的声明式过程建模语言脱颖而出，它提供了一种通过有效迹必须满足的约束集来建模过程的方法，这些约束可以用有限迹上的线性时序逻辑（LTLf）来表达。现有的基于ASP的解决方案通过建模相应的LTLf公式或其等价自动机来编码Declare约束，这可以使用已有技术获得。在本文中，我们引入了一种Declare约束的新颖编码方法，该方法将其语义直接建模为ASP规则，从而消除了对中间表示的需求。我们通过将这种新方法与替代的ASP编码以及一个用于Declare的Python库进行比较，在两个过程挖掘任务上评估了该方法的有效性。本文已提交至《逻辑编程理论与实践》（TPLP）期刊审阅。