论文标题
使用合同检查对法律合同的正式建模和分析
Formal Modeling and Analysis of Legal Contracts using ContractCheck
论文作者
论文摘要
我们描述了一种称为\ textit {ContractCheck}的方法和工具，该方法允许对法律合同的一致性分析，特别是销售购买协议（SPA）。该分析依赖于使用一阶逻辑的可确定片段来执行SPA条款的执行以及所提出的一致性约束。文本水疗中心首先以结构化的自然语言格式编码，称为块。 \ textit {ContractCheck}解释这些块和约束，并将它们翻译成第一型逻辑断言。然后，它调用可满足的模型理论（SMT）求解器，以通过提供令人满意的模型或提供妨碍合同执行的矛盾条款的证据来确定所考虑合同的可执行性。我们说明了\ textit {ContractCheck}的应用，并通过提出未来研究的指示来得出结论。
We describe a method and tool called \textit{ContractCheck} that allows for the consistency analysis of legal contracts, in particular Sales Purchase Agreements (SPAs). The analysis relies on an encoding of the premises for the execution of the clauses of an SPA as well as the proposed consistency constraints using decidable fragments of first-order logic. Textual SPAs are first encoded in a structured natural language format, called blocks. \textit{ContractCheck} interprets these blocks and constraints and translates them in first-oder logic assertions. It then invokes a Satisfiability Modulo Theories (SMT) solver in order to establish the executability of a considered contract by either providing a satisfying model, or by providing evidence of contradictory clauses that impede the execution of the contract. We illustrate the application of \textit{ContractCheck} and conclude by proposing directions for future research.
