Issue 4/2022
Special issue on Six Decades of Automated Reasoning: Papers in Memory of Larry Wos (437-584)
Content (23 Articles)
Larry Wos: Visions of Automated Reasoning
Michael Beeson, Maria Paola Bonacina, Michael Kinyon, Geoff Sutcliffe
Set of Support, Demodulation, Paramodulation: A Historical Perspective
Maria Paola Bonacina
A Comprehensive Framework for Saturation Theorem Proving
Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette
Making Higher-Order Superposition Work
Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, Sophie Tourret
A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column
Sophie Tourret, Christoph Weidenbach
A Formalization of Dedekind Domains and Class Groups of Global Fields
Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, Filippo A. E. Nuccio Mortarino Majno di Capriglio
Local is Best: Efficient Reductions to Modal Logic K
Fabio Papacchini, Cláudia Nalon, Ullrich Hustadt, Clare Dixon
Pardinus: A Temporal Relational Model Finder
Nuno Macedo, Julien Brunel, David Chemouil, Alcino Cunha
From Specification to Testing: Semantics Engineering for Lua 5.2
Mallku Soldevila, Beta Ziliani, Bruno Silvestre
Towards Formalising Schutz’ Axioms for Minkowski Spacetime in Isabelle/HOL
Richard Schmoetten, Jake E. Palmer, Jacques D. Fleuriot
Formalization of the Computational Theory of a Turing Complete Functional Language Model
Thiago Mendonça Ferreira Ramos, Ariane Alves Almeida, Mauricio Ayala-Rincón
A Formalization of the Smith Normal Form in Higher-Order Logic
Jose Divasón, René Thiemann
Correction to: A Formalization of the Smith Normal Form in Higher-Order Logic
Jose Divasón, René Thiemann
Correction to: Local is Best: Efficient Reductions to Modal Logic K
Fabio Papacchini, Cláudia Nalon, Ullrich Hustadt, Clare Dixon