# zbMATH — the first resource for mathematics

MetiTarski: past and future. (English) Zbl 1360.68765
Beringer, Lennart (ed.) et al., Interactive theorem proving. Third international conference, ITP 2012, Princeton, NJ, USA, August 13–15, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-32346-1/pbk). Lecture Notes in Computer Science 7406, 1-10 (2012).
Summary: A brief overview is presented of MetiTarski [B. Akbarpour and the author, J. Autom. Reasoning 44, No. 3, 175–205 (2010; Zbl 1215.68206)], an automatic theorem prover for real-valued special functions: $$\ln$$, $$\exp$$, $$\sin$$, $$\cos$$, etc. MetiTarski operates through a unique interaction between decision procedures and resolution theorem proving. Its history is briefly outlined, along with current projects. A simple collision avoidance example is presented.
For the entire collection see [Zbl 1246.68023].

##### MSC:
 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
MetiTarski
Full Text: