miz3 swMATH ID: 18631 Software Authors: Wiedijk, Freek Description: A synthesis of the procedural and declarative styles of interactive theorem proving. We propose a synthesis of the two proof styles of interactive theorem proving: the procedural style (where proofs are scripts of commands, like in Coq) and the declarative style (where proofs are texts in a controlled natural language, like in Isabelle/Isar). Our approach combines the advantages of the declarative style – the possibility to write formal proofs like normal mathematical text – and the procedural style – strong automation and help with shaping the proofs, including determining the statements of intermediate steps. Our approach is new, and differs significantly from the ways in which the procedural and declarative proof styles have been combined before in the Isabelle, Ssreflect and Matita systems. Our approach is generic and can be implemented on top of any procedural interactive theorem prover, regardless of its architecture and logical foundations. To show the viability of our proposed approach, we fully implemented it as a proof interface called miz3 , on top of the HOL Light interactive theorem prover. The declarative language that this interface uses is a slight variant of the language of the Mizar system, and can be used for any interactive theorem prover regardles s of its logical foundations. The miz3 interface allows easy access to the full set of tactics and formal libraries of HOL Light, and as such has ‘industrial strength’. Our approach gives a way to automatically convert any proced ural proof to a declarative counterpart, where the converted proof is similar in size to the original. As all declarative systems have essentially the same proof language, this give s a straightforward way to port proofs between interactive theorem provers. Homepage: https://arxiv.org/pdf/1201.3601.pdf Related Software: Coq; Mizar; Isar; HOL; Isabelle/HOL; OMDoc; HOL Light; ML; MoMM; SPASS; MPTP 0.2; MPTP; Isabelle/Isar; MizarMode; Flyspeck; Sledgehammer; Metamath; MML; Twelf; E Theorem Prover Cited in: 11 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year A synthesis of the procedural and declarative styles of interactive theorem proving. Zbl 1238.68147Wiedijk, Freek 2012 all top 5 Cited by 30 Authors 3 Grabowski, Adam 2 Kaliszyk, Cezary 2 Korniłowicz, Artur 2 Naumowicz, Adam 2 Pąk, Karol 2 Urban, Josef 1 Alama, Jesse 1 Aravantinos, Vincent 1 Bancerek, Grzegorz 1 Basin, David A. 1 Bezem, Marc 1 Byliński, Czesław 1 Dabrowski, Frédéric 1 Hasan, Osman 1 Janičić, Predrag 1 Khan Afshar, Sanaz 1 Lochbihler, Andreas 1 Loulergue, Frédéric 1 Mahmoud, Mohamed Yousri 1 Matuszewski, Roman 1 Narboux, Julien 1 Pinsard, Thomas 1 Richter, William 1 Seddiki, Ons 1 Sefidgar, S. Reza 1 Siddique, Umair 1 Stojanović Đurđević, Sana 1 Stojanović, Sana 1 Tahar, Sofiène 1 Wiedijk, Freek all top 5 Cited in 7 Serials 3 Journal of Automated Reasoning 1 Journal of Cryptology 1 Annals of Mathematics and Artificial Intelligence 1 Computer Languages, Systems & Structures 1 Mathematics in Computer Science 1 Logical Methods in Computer Science 1 Formalized Mathematics all top 5 Cited in 8 Fields 10 Computer science (68-XX) 6 Mathematical logic and foundations (03-XX) 1 General and overarching topics; collections (00-XX) 1 Geometry (51-XX) 1 Optics, electromagnetic theory (78-XX) 1 Quantum theory (81-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year