Related papers: Proceedings Seventh Workshop on Proof eXchange for…
This volume contains the proceedings of the Combined 23nd International Workshop on Expressiveness in Concurrency and the 13th Workshop on Structural Operational Semantics (EXPRESS/SOS 2016) which was held on 22 August 2016 in Qu\'ebec…
Types for Proofs and Programs is the annual meeting of the Types Project, whose aim is to develop the technology of formal reasoning and computer programming based on Type Theory. This is done by improving the languages and computerised…
The aim of the workshop was to bring together experts working on open-domain dialogue research. In this speedily advancing research area many challenges still exist, such as learning information from conversations, and engaging in a…
This volume contains selected papers from the proceedings of the First International Workshop on Strategies in Rewriting, Proving, and Programming (IWS 2010), which was held on July 9, 2010, in Edinburgh, UK. Strategies are ubiquitous in…
We introduce Prove-It, a Python-based general-purpose interactive theorem-proving assistant designed with the goal of making formal theorem proving as easy and natural as informal theorem proving (with moderate training). Prove-It uses a…
Motivated by the transfer of proofs between proof systems, and in particular from first order automated theorem provers (ATPs) to interactive theorem provers (ITPs), we specify an extension of the TPTP derivation text format to describe…
The SYNT workshop aims to bring together researchers interested in the broad area of synthesis of computing systems. The goal is to foster the development of frontier techniques in automating the development of computing system.…
This EPTCS volume contains the papers from the Sixth International Workshop on Formal Methods for Autonomous Systems (FMAS 2024), which was held between the 11th and 13th of November 2024. FMAS 2024 was co-located with 19th International…
This EPTCS volume contains the joint proceedings for the fourth international workshop on Formal Methods for Autonomous Systems (FMAS 2022) and the fourth international workshop on Automated and verifiable Software sYstem DEvelopment (ASYDE…
This volume contains the proceedings of the First Workshop on Logics and Model-checking for self-* systems (MOD* 2014). The worshop took place in Bertinoro, Italy, on 12th of September 2014, and was a satellite event of iFM 2014 (the 11th…
Theorem proving serves as a major testbed for evaluating complex reasoning abilities in large language models (LLMs). However, traditional automated theorem proving (ATP) approaches rely heavily on formal proof systems that poorly align…
Automated theorem provers and formal proof assistants are general reasoning systems that are in theory capable of proving arbitrarily hard theorems, thus solving arbitrary problems reducible to mathematics and logical reasoning. In…
Theorem proving is a fundamental aspect of mathematics, spanning from informal reasoning in natural language to rigorous derivations in formal systems. In recent years, the advancement of deep learning, especially the emergence of large…
This volume contains a selection of papers presented at the 16th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2-2020). The workshops are the premier technical forum for presenting research and experiences…
Electronic exams (e-exams) have the potential to substantially reduce the effort required for conducting an exam through automation. Yet, care must be taken to sacrifice neither task complexity nor constructive alignment nor grading…
Traditionally, in Programming-by-example (PBE) the goal is to synthesize a program from a small set of input-output examples. Lately, PBE has gained traction as a few-shot reasoning benchmark, relaxing the requirement to produce a program…
This volume contains the proceedings of the Fifth International Workshop on Verification and Program Transformation (VPT 2017). The workshop took place in Uppsala, Sweden, on April 29th, 2017, affiliated with the European Joint Conferences…
Representation determines how we can reason about a specific problem. Sometimes one representation helps us find a proof more easily than others. Most current automated reasoning tools focus on reasoning within one representation. There is,…
Mathematical theorems are human knowledge able to be accumulated in the form of symbolic representation, and proving theorems has been considered intelligent behavior. Based on the BHK interpretation and the Curry-Howard isomorphism, proof…
Automated theorem proving has long been a key task of artificial intelligence. Proofs form the bedrock of rigorous scientific inquiry. Many tools for both partially and fully automating their derivations have been developed over the last…