Publications of L. C. Paulson

• Refereed Articles
  • Isabelle
  • Security Protocols
  • Automation
  • MetiTarski Prover
  • Set Theory
  • UNITY Formalism
  • Induction / Recursion
  • LCF and HOL Systems
• Workshop Papers
• Misc Papers
• Lecture Courses
  • Foundations of Computer Science
  • Logic and Proof
• Books

The MetiTarski Theorem Prover

MetiTarski is an automatic theorem prover based on a combination of resolution and a decision procedure for the theory of real closed fields. It is designed to prove theorems involving real-valued special functions such as log, exp, sin, cos and sqrt. In particular, it is designed to prove universally quantified inequalities involving such functions. This problem is undecidable, and MetiTarski is incomplete.

You can try out MetiTarski without installing it using System on TPTP. (However, this service does not support MetiTarski's infix notation; see this sample problem.)

MetiTarski is described in the following papers:

1. Behzad Akbarpour and L. C. Paulson.
   Towards Automatic Proofs of Inequalities Involving Elementary Functions. In: Byron Cook and Roberto Sebastiani (editors), PDPAR 2006: Pragmatics of Decision Procedures in Automated Reasoning, 27–37.
2. Behzad Akbarpour and Lawrence C. Paulson.
   Extending a Resolution Prover for Inequalities on Elementary Functions. In: Nachum Dershowitz and Andrei Voronkov (editors), Logic for Programming, Artificial Intelligence, and Reasoning — LPAR 2007 (Springer LNCS 4790), 47–61. Publisher's version
3. Behzad Akbarpour and L. C. Paulson.
   MetiTarski: An Automatic Prover for the Elementary Functions. In: Serge Autexier et al. (editors), Intelligent Computer Mathematics (Springer LNCS 5144, 2008), 217–231. (Proceedings of Calculemus 2008.) Publisher's version
   Slides available.
4. Behzad Akbarpour and L. C. Paulson.
   Applications of MetiTarski in the Verification of Control and Hybrid Systems. In: Rupak Majumdar and Paulo Tabuada (editors), Hybrid Systems: Computation and Control (Springer LNCS 5469, 2009), 1–15. Publisher's version
5. Behzad Akbarpour and L. C. Paulson.
   MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions. J. Automated Reasoning 44 3 (2010), 175–205. Publisher's version
6. William Denman, Behzad Akbarpour, Sofiène Tahar, Mohamed H. Zaki and L. C. Paulson.
   Formal Verification of Analog Designs using MetiTarski.
   In: Armin Biere and Carl Pixley (editors), Formal Methods in Computer Aided Design (2009), 93–100. Publisher's version
7. Rajeev Narayanan, Behzad Akbarpour, Mohamed H. Zaki, Sofiène Tahar and L. C. Paulson.
   Formal Verification of Analog Circuits in the Presence of Noise and Process Variation. In: DATE 2010: Design, Automation and Test in Europe, in press.

MetiTarski (version 1.3, 25 February 2010) is available to download. Please note that it is experimental research software and will require a certain amount of effort to build on your machine. In particular, you will need to download and install two further pieces of software:

• The Poly/ML compiler
• The decision procedure QEPCAD (Mac users can find a precompiled binary here)

If you have difficulties using MetiTarski, I would be happy to help. In return I hope you can provide advice on how to improve it, sample problems, applications, etc.

Research funded by the EPSRC grant EP/C013409/1, Beyond Linear Arithmetic. MetiTarski is a modified version of Joe Hurd's Metis prover.

Lawrence C. Paulson