通过不可满足性证明诊断带关系对象的一阶逻辑
Diagnosis via Proofs of Unsatisfiability for First-Order Logic with Relational Objects
AI总结：
针对FOL*不可满足性结果的正确性验证与原因解释问题，本文提出UNSAT证明格式、证明规则、证明验证算法及基于证明的诊断，并在FOL*检查器上实现验证。
摘要：
基于可满足性的自动推理是一种在软件工程中被成功用于验证复杂软件（包括安全关键系统）的方法。此类推理支撑着许多验证活动，从需求分析到设计一致性再到测试覆盖率。尽管通常有效，但后端约束求解器往往很复杂且不可避免地容易出错，这威胁到其应用的可靠性。因此，此类求解器需要被验证，其中包括检查正确性并解释它们返回的（不）可满足性结果。在本工作中，我们考虑基于带关系对象的一阶逻辑（First-Order Logic with relational objects，FOL*）的可满足性分析，该逻辑已被证明能有效推理时间和数据敏感的早期系统设计。我们应对验证FOL*不可满足性结果的正确性并推导诊断以解释不可满足性原因的挑战。受SAT/SMT求解器的UNSAT证明概念启发，我们定义了一种证明格式和证明规则，以将求解器的推理步骤追踪为通向UNSAT的推导序列。我们还提出了一种算法，用于验证FOL*证明的正确性，同时过滤不必要的推导，并开发了一种基于证明的诊断来解释不可满足性的原因。我们在最先进的FOL*可满足性检查器之上实现了所提出的证明支持，以生成UNSAT证明，并通过应用基于证明的诊断来解释软件系统规范性需求的良构性问题的原因，验证了我们的方法。
英文摘要：
Satisfiability-based automated reasoning is an approach that is being successfully used in software engineering to validate complex software, including for safety-critical systems. Such reasoning underlies many validation activities, from requirements analysis to design consistency to test coverage. While generally effective, the back-end constraint solvers are often complex and inevitably error-prone, which threatens the soundness of their application. Thus, such solvers need to be validated, which includes checking correctness and explaining (un)satisfiability results returned by them. In this work, we consider satisfiability analysis based on First-Order Logic with relational objects (FOL*) which has been shown to be effective for reasoning about time- and data-sensitive early system designs. We tackle the challenge of validating the correctness of FOL* unsatisfiability results and deriving diagnoses to explain the causes of the unsatisfiability. Inspired by the concept of proofs of UNSAT from SAT/SMT solvers, we define a proof format and proof rules to track the solvers' reasoning steps as sequences of derivations towards UNSAT. We also propose an algorithm to verify the correctness of FOL* proofs while filtering unnecessary derivations and develop a proof-based diagnosis to explain the cause of unsatisfiability. We implemented the proposed proof support on top of the state-of-the-art FOL* satisfiability checker to generate proofs of UNSAT and validated our approach by applying the proof-based diagnoses to explain the causes of well-formedness issues of normative requirements of software systems.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
