Copyright: University of Konstanz/Tadeo Berner

Contract check at the push of a button

Pioneering work in law and computer science project: using a logic-based model to automatically test company purchase agreements for inconsistencies. The project is conducted at the Centre for Human | Data | Society at the University of Konstanz.

If the ownership of a company changes, this can result in a purchase agreement of several hundred pages. Not only are such contracts long, but also their content is very complex. Negotiations take a lot of time and many people are involved in drafting the agreements, which get amended all the time. It is hard to keep track of everything. The risk of undiscovered contradictions, incorrect references, missing clauses or requirements that cannot be fulfilled is high. It's like playing memory: If you flip over a card, you need to know where the corresponding counterpart is located to avoid a mismatch.

Rüdiger Wilhelmi knows the problem from experience. Before being appointed as a professor of civil law, commercial, corporate and business law as well as comparative law at the University of Konstanz, he worked in the legal department of a large industrial company, where he negotiated such agreements. Back then, he "manually" scanned them for errors. Together with computer scientist Stefan Leue, he is now developing the "ContractCheck" model, which can analyze company purchase agreements fully automatically for inconsistencies.

Stefan Leue, professor of software and systems engineering at the University of Konstanz, compares the tool to the spell and grammar checker of a writing programme that indicates errors by underlining them. Company purchase agreements are particularly suitable for such a model, as they often consist of very similar blocks of text that differ only in specific details, such as price. "In the case of international acquisitions, it is estimated that about half of the text is changed only little or not at all in terms of provisions", Wilhelmi says. In addition, company purchase agreements are usually relatively isolated texts, which eliminates further complexity generated by the legal environment.

Typical clauses have to be translated into logical blocks
The law team was faced with the task of identifying typical clauses in a specially created sample contract and translating these into logical blocks. In this process, questions came up like: What are the components of a contract, what are their structures, what is the logical relationship between the different parts? To formalize these logical dependencies, the computer scientists chose a description technique based on propositional logic and "decidable" parts of first-order logic. This way, logical statements that can be answered with "yes" or "no" can be attributed to each block of a legal contract. Algorithms, in turn, can then check, virtually at the push of a button, whether a logical system, and thus a contract, is consistent or not", explains Leue.

Implicit knowledge must become explicit
These contract blocks deal, for example, with the name of the buyer, the object of purchase or the purchase price. Very complex parts of the formalization have to factor in the concept of law and contractual practice. Another example of the special challenge for the logical formalization is the human ability to make legal assessments, i.e. "the lawyers' gut feeling", as Wilhelmi calls it. This tacit knowledge has to be made explicit for formalization, requiring a constant exchange between law and computer science, which prove to be advantageous for both disciplines. "It was a very fruitful collaboration, because we had to make decisions for situations that we had never thought about before, as something like that had never come up in a real case", the lawyer says. Computer science, on the other hand, also benefited by adapting the techniques of software engineering to other areas and thus expanding the scope of application.

Putting humans centre stage
As with any abstraction, details are lost in the formalization of business purchase agreements. The researchers assume that there will always be areas where the model works and where it is – possibly necessarily – fuzzy. This is quite intentional. Rüdiger Wilhelmi says: "There will be tools that help humans to automate traditional legal activities, but they won't succeed in completely replacing humans".

The research team around the two professors includes staff from computer science and law, and is conducting the project in the context of the Centre for Human | Data | Society. Andreas Spitz, junior professor of data and information mining, complements the team, that is currently testing, on the basis of their prototype, whether artificial intelligence methods can be used to automatically derive the block structure or the individual modules from the contracts. For this purpose, the researchers have planned to train an existing language model with sample contracts. Stefan Leue adds: "We don't want to replace jurisprudence with artificial intelligence methods. No legal decisions are to be prepared or even made. We put humans centre stage".

The Centre for Human | Data | Society
The Centre for Human | Data | Society (CHDS) was founded at the University of Konstanz in autumn 2022. At the centre, researchers investigate the processes of digitalization and datafication in our (data) society, with a principal focus on humans: What interactions are there between people and the data society? What kind of data society do we really want, and how should it be designed? To answer these questions, the CHDS team employs a transdisciplinary approach, analyzing technical, legal, political, psychological, media-cultural, historical, economic and social aspects of the data society.

Key facts:

  • Project cooperation between law and computer science has developed a logic-based model to test corporate purchase agreements for inconsistencies
  • The description technique of the contract parts is based on propositional logic and "decidable" parts of first-order logic
  • Development of algorithm that can automatically determine whether a contract is consistent
  • In a second step, artificial intelligence methods are used to test whether the block structure or the individual modules can be automatically derived from contracts
  • More information on the Centre for Human | Data | Society (CHDS):