How can we support the development of reliable software by theorem proving techniques? How can we turn machine-generated proofs into proofs that can be comprehensed by mathematicians and programmers? This book addresses these questions by presenting an efficient method for transforming proofs generated by matrix-based proof procedures into sequent-style proofs, which works uniformly for classical and non-classical logics. It is a significant contribution towards making theorem proving technology useful for mathematics and software development practice.
26th European Conference on Artificial Intelligence, September 30 – October 4, 2023, Kraków, Poland – Including 12th Conference on Prestigious Applications of Intelligent Systems (PAIS 2023)
