相关论文: Proceedings 10th International Workshop on the ACL…

This volume contains the proceedings of the First International Workshop of Formal Techniques for Safety-Critical Systems (FTSCS 2012), held in Kyoto on November 12, 2012, as a satellite event of the ICFEM conference. The aim of this…

Over the past years there has been quite a lot of activity in the algebraic community about using algebraic methods for providing support to model-driven software engineering. The aim of this workshop is to gather researchers working on the…

Large Language Models (LLMs) present an intriguing avenue for exploration in the field of formal theorem proving. Nevertheless, their full potential, particularly concerning the mitigation of hallucinations and refinement through prover…

This special issue cover the seventh and last conference of the CL&C series, started in 2006 in San Servolo. Topics are the computational content of logics between intuitionistic logic and classical logic, through normalization, and a new…

The ThEdu series pursues the smooth transition from an intuitive way of doing mathematics at secondary school to a more formal approach to the subject in STEM education, while favouring software support for this transition by exploiting the…

This volume contains the papers presented at LN2FR 2022: The International Workshop on Methodologies for Translating Legal Norms into Formal Representations, held on December 14, 2022 in association with 35th International Conference on…

DCM 2010 provides a forum for ideas about new computing means and models, with a particular emphasis in 2010 on computational and causal models related to physics and biology. We believe that bringing together different approaches - in a…

We present Ax-Prover, a multi-agent system for automated theorem proving in Lean that can solve problems across diverse scientific domains and operate either autonomously or collaboratively with human experts. To achieve this, Ax-Prover…

Behavioral synthesis involves compiling an Electronic System-Level (ESL) design into its Register-Transfer Level (RTL) implementation. Loop pipelining is one of the most critical and complex transformations employed in behavioral synthesis.…

This volume contains the proceedings of the 11th International Workshop on Quantum Physics and Logic (QPL 2014), which was held from the 4th to the 6th of June, 2014, at Kyoto University, Japan. The goal of the QPL workshop series is to…

We present a prototype of an integrated reasoning environment for educational purposes. The presented tool is a fragment of a proof assistant and automated theorem prover. We describe the existing and planned functionality of the theorem…

We introduce a proof recommender system for the HOL4 theorem prover. Our tool is built upon a transformer-based model [2] designed specifically to provide proof assistance in HOL4. The model is trained to discern theorem proving patterns…

The aim of the INFINITY workshop is to provide a forum for researchers interested in the development of formal methods and algorithmic techniques for the analysis of systems with infinitely many states, and their application in automated…

The theory of asymptotic complexity provides an approach to characterizing the behavior of programs in terms of bounds on the number of computational steps executed or use of computational resources. We describe work using ACL2 to prove…

The workshop series intends to cover research that investigates the computational aspects of classical logic and mathematics. Its focus is on unwinding the computational content of logical principles and proof in mathematics based on these…

This volume contains a selection of the papers presented at TERMGRAPH 2018, the tenth edition of the international workshop on computing with terms and graphs. Graphs, and graph transformation systems, are used in many areas within Computer…

This paper reports our initial experiments with using external ATP on some corpora built with the ACL2 system. This is intended to provide the first estimate about the usefulness of such external reasoning and AI systems for solving ACL2…

Classical Logic and Computation (CL&C) 2014 is the fifth edition of this workshop series. The workshop series intends to cover all work aiming to explore computational aspects of classical logic and mathematics. Its focus is on the…

This volume contains the proceedings of the Tenth International Workshop on Fixed Points in Computer Science (FICS 2015) which took place on September 11th and 12th, 2015 in Berlin, Germany, as a satellite event of the conference Computer…

This volume contains the joint post-proceedings of the 2015 edition of the ML Family Workshop and OCaml Users and Developers Workshop, held in Vancouver, British Columbia, Canada, in affiliation with ICFP 2015.