Skip to main content
SpringerLink
Log in

Automated Consistency Analysis for Legal Contracts

  • Conference paper
  • First Online:
Model Checking Software (SPIN 2022)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 13255))

Included in the following conference series:

  • 349 Accesses

Abstract

Contracts in business life, and in particular company purchase agreements, often comprise a large number of provisions and are correspondingly long and complex. In practice, it is therefore a great challenge to keep track of their regulatory context and to identify and avoid inconsistencies in such contracts. Against this background, we propose a semi-formal as well as a formal logical modeling of this type of contracts, using decidable first-order theories. We also present the tool ContractCheck, which performs fully automated inconsistency analyses on the considered contracts using Satisfiability Modulo Theories (SMT) solving.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    We set legal terms in italics and terms referring to UML diagrams in teletype font.

References

  1. Balbiani, P., Broersen, J.M., Brunel, J.: Decision procedures for a deontic logic modeling temporal inheritance of obligations. Electron. Notes Theor. Comput. Sci. 231, 69–89 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  2. Bürgerliches Gesetzbuch, German Civil Code

    Google Scholar 

  3. Braegelmann, T., Kaulartz, M.: Rechtshandbuch Smart Contracts. C. H. Beck, Munich (2019)

    Google Scholar 

  4. Bonifacio, A.L., Della Mura, W.A.: Automatically running experiments on checking multi-party contracts. Artif. Intell. Law 29(3), 287–310 (2020). https://doi.org/10.1007/s10506-020-09276-y

    Article  Google Scholar 

  5. Boley, H., Paschke, A., Shafiq, O.: RuleML 1.0: the overarching specification of web rules. In: Dean, M., Hall, J., Rotolo, A., Tabet, S. (eds.) RuleML 2010. LNCS, vol. 6403, pp. 162–178. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16289-3_15

    Chapter  Google Scholar 

  6. ContractCheck (2022). https://github.com/sen-uni-kn/ContractCheck

  7. Castro, P.F., Maibaum, T.S.E.: A complete and compact propositional deontic logic. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol. 4711, pp. 109–123. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-75292-9_8

    Chapter  Google Scholar 

  8. Castro, P.F., Maibaum, T.S.E.: A tableaux system for deontic action logic. In: van der Meyden, R., van der Torre, L. (eds.) DEON 2008. LNCS (LNAI), vol. 5076, pp. 34–48. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70525-3_4

    Chapter  MATH  Google Scholar 

  9. Camilleri, J.J., Schneider, G.: Modelling and analysis of normative documents. J. Log. Algebraic Methods Program. 91, 33–59 (2017)

    Article  MathSciNet  MATH  Google Scholar 

  10. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  11. Desai, N., Narendra, N.C., Singh, M.P.: Checking correctness of business contracts via commitments. In: AAMAS (2), pp. 787–794. IFAAMAS (2008)

    Google Scholar 

  12. Engers, T., Gerrits, R., Boekenoogen, M., Glassée, E., Kordelaar, P.: Power: using UML/OCL for modeling legislation - an application report. In: 8th International Conference on Artificial Intelligence and Law, pp. 157–167. Association for Computing Machinery (2001)

    Google Scholar 

  13. Faciano, C., et al.: Performance improvement on legal model checking. In: ICAIL, pp. 59–68. ACM (2017)

    Google Scholar 

  14. Gorín, D., Mera, S., Schapachnik, F.: Model checking legal documents. In: JURIX, Frontiers in Artificial Intelligence and Applications, vol. 223, pp. 151–154. IOS Press (2010)

    Google Scholar 

  15. Gorín, D., Mera, S., Schapachnik, F.: A software tool for legal drafting. In: FLACOS, EPTCS, vol. 68, pp. 71–86 (2011)

    Google Scholar 

  16. Grupp, M.: Wie baut man einen rechtsautomaten? In: Hartung, M., Bues, M.-M., Halbleib, G. (eds.) Legal Tech, edge number: 1110. C.H. Beck (2018)

    Google Scholar 

  17. Gebele, A., Scholz, K.-S. (eds.): Beck’sches Formularbuch Bürgerliches, Handels- und Wirtschaftsrecht, 14th edn. C.H. Beck (2022)

    Google Scholar 

  18. Hvitved, T., Klaedtke, F., Zalinescu, E.: A trace-based model for multiparty contracts. J. Log. Algebraic Methods Program. 81(2), 72–98 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  19. Henglein, F., Larsen, C.K., Murawska, A.: A formally verified static analysis framework for compositional contracts. In: Bernhard, M., et al. (eds.) FC 2020. LNCS, vol. 12063, pp. 599–619. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-54455-3_42

    Chapter  Google Scholar 

  20. Hill, C.A., Solomon, S.D.: Research Handbook on Mergers and Acquisitions. Edward Elgar Publishing, Cheltenham (2016)

    Google Scholar 

  21. Kabilan, V.: Contract workflow model patterns using BPMN. In: EMMSAD, CEUR Workshop Proceedings, vol. 363, pp. 171–182 (2005). CEUR-WS.org

  22. Kabilan, V., Johannesson, P.: Semantic representation of contract knowledge using multi tier ontology. In: Cruz, I.F. Kashyap, V., Decker, S., Eckstein, R. (eds.) Proceedings of SWDB 2003, The First International Workshop on Semantic Web and Databases, Co-Located with VLDB 2003, Humboldt-Universität, Berlin, Germany, 7–8 September 2003, pp. 395–414 (2003)

    Google Scholar 

  23. Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View. Texts in Theoretical Computer Science. An EATCS Series, 2nd edn. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-540-74105-3

  24. Mura, W.A.D., Bonifácio, A.L.: Devising a conflict detection method for multi-party contracts. In: SCCC, pp. 1–6. IEEE (2015)

    Google Scholar 

  25. Martínez, E., Díaz, G., Cambronero, M.-E., Schneider, G.: A model for visual specification of e-contracts. In: IEEE SCC, pp. 1–8. IEEE Computer Society (2010)

    Google Scholar 

  26. Madaan, N., Radha Krishna, P., Karlapalem, K.: Consistency detection in e-contract documents. In: ICEGOV, pp. 267–274. ACM (2014)

    Google Scholar 

  27. Meyer-Sparenberg, W.: Unternehmenskaufvertrag (gmbh-anteile) - käuferfreundlich. In: Gebele, A., Scholz, K.-S. (eds.) Beck’sches Formularbuch Bürgerliches, Handels- und Wirtschaftsrecht. C.H. Beck (2022)

    Google Scholar 

  28. Meyer-Sparenberg, W.: Unternehmenskaufvertrag (gmbh-anteile) - verkäuferfreundlich. In: Gebele, A., Scholz, K.-S. (eds.) Beck’sches Formularbuch Bürgerliches, Handels- und Wirtschaftsrecht. C.H. Beck (2022)

    Google Scholar 

  29. Meyer-Sparenberg, W., Jäckle, C. (eds.): Beck’sches M &A-Handbuch: Planung, Gestaltung, Sonderformen, regulatorische Rahmenbedingungen und Streitbeilegung bei Mergers & Acquisitions, 2nd edn. C.H. Beck (2022)

    Google Scholar 

  30. OASIS Standard: LegalRuleML, version 1.0 (2021). https://docs.oasis-open.org/legalruleml/legalruleml-core-spec/v1.0/os/legalruleml-core-spec-v1.0-os.pdf

  31. Object Management Group: Business Process Model and Notation 2014. https://www.omg.org/spec/BPMN

  32. Object Management Group: Unified Modelling Language, Specification 2.5.1 (2017). http://www.omg.org/spec/UML

  33. Boris, P.: Paal and Martin Fries. Smart Contracts, Mohr Siebeck (2019)

    Google Scholar 

  34. Pfisterer, B.: Share deal. In: Weise, S., Krauß, H.-F. (eds.) Beck’sche Online-Formulare. C.H. Beck (2022)

    Google Scholar 

  35. Palmirani, M., Governatori, G., Rotolo, A., Tabet, S., Boley, H., Paschke, A.: LegalRuleML: XML-based rules and norms. In: Olken, F., Palmirani, M., Sottara, D. (eds.) RuleML 2011. LNCS, vol. 7018, pp. 298–312. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24908-2_30

    Chapter  Google Scholar 

  36. Pace, G., Prisacariu, C., Schneider, G.: Model checking contracts – a case study. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 82–97. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-75596-8_8

    Chapter  Google Scholar 

  37. Prisacariu, C., Schneider, G.: A formal language for electronic contracts. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol. 4468, pp. 174–189. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-72952-5_11

    Chapter  MATH  Google Scholar 

  38. Prisacariu, C., Schneider, G.: A dynamic deontic logic for complex contracts. J. Log. Algebraic Methods Program. 81(4), 458–490 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  39. Seibt, C.H. (ed.): Beck’sches Formularbuch Mergers & Acquisitions, 3rd edn. C.H. Beck (2018)

    Google Scholar 

  40. Seibt, C.H.: GmbH-Anteilskaufvertrag - ausführlich, käuferfreundlich. In: Beck’sches Formularbuch Mergers & Acquisitions, pp. 324–456. C.H. Beck (2018)

    Google Scholar 

  41. Seibt, C.H.: Gmbh-anteilskaufvertrag - ausführlich, verkäuferfreundlich, deutsch. In: Beck’sches Formularbuch Mergers & Acquisitions, pp. 233–323. C.H. Beck, München (2018)

    Google Scholar 

  42. Seibt, C.H.: Gmbh-anteilskaufvertrag - knapp, ausgewogen. In: Beck’sches Formularbuch Mergers & Acquisitions, pp. 515–525. C.H. Beck (2018)

    Google Scholar 

  43. Seibt, C.H.: Gmbh-anteilskaufvertrag - knapp, verkäuferfreundlich. In: Beck’sches Formularbuch Mergers & Acquisitions, pp. 457–514. C.H. Beck (2018)

    Google Scholar 

  44. von Hoyenberg, P.: Share deal (GmbH, fester kaufpreis). In: Weipert, L., Arnhold, P., Baltus, M. (eds.) Münchener Vertragshandbuch, pp. 228–233. C.H. Beck (2020)

    Google Scholar 

  45. von Hoyenberg, P.: Share deal (GmbH, mit stichtagsbilanzierung). In: Weipert, L., Arnhold, P., Baltus, M. (eds.) Münchener Vertragshandbuch, Beck-online Bücher, pp. 203–227. C.H. Beck (2020)

    Google Scholar 

  46. Wright, G.H.V.: Deontic logic. Mind 60(237), 1–15 (1951)

    Article  Google Scholar 

  47. Weipert, L., Arnhold, P., Baltus, M. (eds.): Münchener Vertragshandbuch: Band 2, 8th edn. C.H. Beck (2020)

    Google Scholar 

  48. Wilhelmi, R.: §453. In: Gsell, B., Krüger, W., Lorenz, S., Reymann, C. (eds.) Beck’scher Online Großkommentar, edge note: 744–782. C.H. Beck (2022)

    Google Scholar 

  49. Weise, S., Krauß, H.-F. (eds.): Beck’sche Online-Formulare: Vertrag. C.H. Beck (2022)

    Google Scholar 

  50. Wan, F., Singh, M.P.: Formalizing and achieving multiparty agreements via commitments. In: AAMAS, pp. 770–777. ACM (2005)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Konstanz, Konstanz, Germany

    Martin Kölbl & Stefan Leue

  2. Department of Law, University of Konstanz, Konstanz, Germany

    Alan Khoja & Rüdiger Wilhelmi

Authors
  1. Alan Khoja
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Martin Kölbl
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Stefan Leue
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Rüdiger Wilhelmi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Martin Kölbl .

Editor information

Editors and Affiliations

  1. Cornell University, Ithaca, NY, USA

    Owolabi Legunsen

  2. University of Illinois Urbana-Champaign, Urbana, IL, USA

    Grigore Rosu

Appendix

Appendix

Text of Bakery SPA

§1 Main Content

1.1 The Seller Anna hereby sells the shares of Bakery AG with all rights and obligations pertaining thereto (including the dividend right for the current financial year), to the Purchaser Chris who accepts such sale. 1.2 The purchaser pays the purchase price 40.000€ to the seller.

1.3 If the transfer is not performed, the Purchaser has the right to withdraw.

1.4 If the pay is not performed, the Seller has the right to withdraw.

§2 The Seller hereby represents and warrants to the Purchaser in the form of an independent guarantee pursuant to Sect. 311 (1) of the German Civil Code and exclusively in accordance with the provisions of this Agreement that the following statements (the “Warranties”) are true and correct as of the date of this Agreement and that the warranties set forth in this paragraph will also be true and correct as of the Closing Date:

2.1 The company can produce at least the 10.000 of Pretzels every day (Pretzel Warranty). In case of the breach of the warranty, it needs to be asserted within 14 days.

§3 The Purchaser’s rights arising from any inaccuracy of any of the Warranties contained in §1 shall be limited to supplementary performance claims and compensation claims against the Seller, subject to the provisions of

3.1 In case the Pretzel Warranty is not met and then the creditor may demand subsequent performance within 28 business days from the debtor after having transfered the shares.

3.2 In case the Pretzel Warranty is not met and the damage is above 1000€ then a compensation of 100€ per 100 pretzels not baked pretzels is paid within 14 business days.

§4 Claims of §3 expire after 42 business days.

§5 The Bakery AG is transferred by way of security to Bank B.

Text Blocks of Bakery SPA

figure a

Rights and permissions

Reprints and permissions

Copyright information

© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Khoja, A., Kölbl, M., Leue, S., Wilhelmi, R. (2022). Automated Consistency Analysis for Legal Contracts. In: Legunsen, O., Rosu, G. (eds) Model Checking Software. SPIN 2022. Lecture Notes in Computer Science, vol 13255. Springer, Cham. https://doi.org/10.1007/978-3-031-15077-7_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-15077-7_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-15076-0

  • Online ISBN: 978-3-031-15077-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation