No Arabic abstract
The 9th International Workshop on Theorem-Proving Components for Educational Software (ThEdu20) was scheduled to happen on June 29 as a satellite of the IJCAR-FSCD 2020 joint meeting, in Paris. The COVID-19 pandemic came by surprise, though, and the main conference was virtualised. Fearing that an online meeting would not allow our community to fully reproduce the usual face-to-face networking opportunities of the ThEdu initiative, the Steering Committee of ThEdu decided to cancel our workshop. Given that many of us had already planned and worked for that moment, we decided that ThEdu20 could still live in the form of an EPTCS volume. The EPTCS concurred with us, recognising this very singular situation, and accepted our proposal of organising a special issue with papers submitted to ThEdu20. An open call for papers was then issued, and attracted five submissions, all of which have been accepted by our reviewers, who produced three careful reports on each of the contributions. The resulting revised papers are collected in the present volume. We, the volume editors, hope that this collection of papers will help further promoting the development of theorem-proving-based software, and that it will collaborate to improve the mutual understanding between computer mathematicians and stakeholders in education. With some luck, we would actually expect that the very special circumstances set up by the worst sanitary crisis in a century will happen to reinforce the need for the application of certified components and of verification methods for the production of educational software that would be available even when the traditional on-site learning experiences turn out not to be recommendable.
This volume of EPTCS contains the proceedings of the Sixth Workshop on Proof Exchange for Theorem Proving (PxTP 2019), held on 26 August 2019 as part of the CADE-27 conference in Natal, Brazil. The PxTP workshop series brings together researchers working on various aspects of communication, integration, and cooperation between reasoning systems and formalisms, with a special focus on proofs. The progress in computer-aided reasoning, both automated and interactive, during the past decades, made it possible to build deduction tools that are increasingly more applicable to a wider range of problems and are able to tackle larger problems progressively faster. In recent years, cooperation between such tools in larger systems has demonstrated the potential to reduce the amount of manual intervention. Cooperation between reasoning systems relies on availability of theoretical formalisms and practical tools to exchange problems, proofs, and models. The PxTP workshop series strives to encourage such cooperation by inviting contributions on all aspects of cooperation between reasoning tools, whether automatic or interactive.
This volume of EPTCS contains the proceedings of the Seventh Workshop on Proof Exchange for Theorem Proving (PxTP 2021), held on 11 July 2021 as part of the CADE-28 online conference in Pittsburgh, USA. The PxTP workshop series brings together researchers working on various aspects of communication, integration, and cooperation between reasoning systems and formalisms, with a special focus on proofs. The progress in computer-aided reasoning, both automated and interactive, during the past decades, made it possible to build deduction tools that are increasingly more applicable to a wider range of problems and are able to tackle larger problems progressively faster. In recent years, cooperation between such tools in larger systems has demonstrated the potential to reduce the amount of manual intervention. Cooperation between reasoning systems relies on availability of theoretical formalisms and practical tools to exchange problems, proofs, and models. The PxTP workshop series strives to encourage such cooperation by inviting contributions on all aspects of cooperation between reasoning tools, whether automatic or interactive.
The previous VPT 2020 workshop was organized in honour of Professor Alberto Pettorossi on the occasion of his academic retirement from Universit`a di Roma Tor Vergata. Due to the pandemic the VPT 2020 meeting was cancelled but its proceeding have already appeared in the EPTCS 320 volume. The joint VPT-20-21 event has subsumed the original programme of VPT 2020 and provided an opportunity to meet and celebrate the achievements of Professor Alberto Pettorossi; its programme was further expanded with the newly submitted presentations for VPT 2021. The aim of the VPT workshop series is to provide a forum where people from the areas of program transformation and program verification can fruitfully exchange ideas and gain a deeper understanding of the interactions between those two fields.
This volume contains papers presented at the Ninth International Symposium on Symbolic Computation in Software Science, SCSS 2021. Symbolic Computation is the science of computing with symbolic objects (terms, formulae, programs, representations of algebraic objects, etc.). Powerful algorithms have been developed during the past decades for the major subareas of symbolic computation: computer algebra and computational logic. These algorithms and methods are successfully applied in various fields, including software science, which covers a broad range of topics about software construction and analysis. Meanwhile, artificial intelligence methods and machine learning algorithms are widely used nowadays in various domains and, in particular, combined with symbolic computation. Several approaches mix artificial intelligence and symbolic methods and tools deployed over large corpora to create what is known as cognitive systems. Cognitive computing focuses on building systems that interact with humans naturally by reasoning, aiming at learning at scale. The purpose of SCSS is to promote research on theoretical and practical aspects of symbolic computation in software science, combined with modern artificial intelligence techniques. These proceedings contain the keynote paper by Bruno Buchberger and ten contributed papers. Besides, the conference program included three invited talks, nine short and work-in-progress papers, and a special session on computer algebra and computational logic. Due to the COVID-19 pandemic, the symposium was held completely online. It was organized by the Research Institute for Symbolic Computation (RISC) of the Johannes Kepler University Linz on September 8--10, 2021.
This volume contains the proceedings of the ninth workshop on Quantum Physics and Logic (QPL2012) which took place in Brussels from the 10th to the 12th of October 2012. QPL2012 brought together researchers working on mathematical foundations of quantum physics, quantum computing, and spatio-temporal causal structures. The particular focus was on the use of logical tools, ordered algebraic and category-theoretic structures, formal languages, semantical techniques, and other computer science methods for the study of physical behaviour in general.