arXiv subjects

Haniel Barbosa

Publications and source records attributed to Haniel Barbosa.

9 recordsLinked to original sources

arXiv2026

Hint-Based SMT Proof Reconstruction

There are several paradigms for integrating interactive and automated theorem provers, combining the convenience of powerful automation with strong soundness guarantees. We introduce a new approach for reconstructing proofs found by SMT solvers which we intend to be complementary with existing techniques. Rather than verifying or replaying a full proof produced by the SMT solver, or at the other extreme, rediscovering the solver's proof from just the set of premises it uses, we explore an approach which helps guide an interactive theorem prover's internal automation by leveraging derived facts during solving, which we call hints. This makes it possible to extract more information from the SMT solver's proof without the cost of retaining a dependency on the SMT solver itself. We implement a tactic in the Lean proof assistant, called QuerySMT, which leverages hints from the cvc5 SMT solver to improve existing Lean automation. We evaluate QuerySMT's performance on relevant Lean benchmarks, compare it to other tools available in Lean relating to SMT solving, and show that the hints generated by cvc5 produce a clear improvement in existing automation's performance.

cs.LO↗

arXiv2025

Proceedings Twentieth International Symposium on Logical and Semantic Frameworks with Applications

This volume contains the proceedings of the 20th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2025), which was held in Brasilia, the capital of Brazil, from October 7 to October 8, 2025. The aim of the LSFA series of workshops is bringing together theoreticians and practitioners to promote new techniques and results, from the theoretical side, and feedback on the implementation and use of such techniques and results, from the practical side. LSFA includes areas such as proof and type theory, equational deduction and rewriting systems, automated reasoning and concurrency theory.

cs.LO↗

arXiv2025

Lean-SMT: An SMT tactic for discharging proof goals in Lean

Lean is an increasingly popular proof assistant based on dependent type theory. Despite its success, it still lacks important automation features present in more seasoned proof assistants, such as the Sledgehammer tactic in Isabelle/HOL. A key aspect of Sledgehammer is the use of proof-producing SMT solvers to prove a translated proof goal and the reconstruction of the resulting proof into valid justifications for the original goal. We present Lean-SMT, a tactic providing this functionality in Lean. We detail how the tactic converts Lean goals into SMT problems and, more importantly, how it reconstructs SMT proofs into native Lean proofs. We evaluate the tactic on established benchmarks used to evaluate Sledgehammer's SMT integration, with promising results. We also evaluate Lean-SMT as a standalone proof checker for proofs of SMT-LIB problems. We show that Lean-SMT offers a smaller trusted core without sacrificing too much performance.

cs.LO↗

arXiv2021

Alethe: Towards a Generic SMT Proof Format (extended abstract)

The first iteration of the proof format used by the SMT solver veriT was presented ten years ago at the first PxTP workshop. Since then the format has matured. veriT proofs are used within multiple applications, and other solvers generate proofs in the same format. We would now like to gather feedback from the community to guide future developments. Towards this, we review the history of the format, present our pragmatic approach to develop the format, and also discuss problems that might arise when other solvers use the format.

cs.LO↗

arXiv2021

Fair and Adventurous Enumeration of Quantifier Instantiations

SMT solvers generally tackle quantifiers by instantiating their variables with tuples of terms from the ground part of the formula. Recent enumerative approaches for quantifier instantiation consider tuples of terms in some heuristic order. This paper studies different strategies to order such tuples and their impact on performance. We decouple the ordering problem into two parts. First is the order of the sequence of terms to consider for each quantified variable, and second is the order of the instantiation tuples themselves. While the most and least preferred tuples, i.e. those with all variables assigned to the most or least preferred terms, are clear, the combinations in between allow flexibility in an implementation. We look at principled strategies of complete enumeration, where some strategies are more fair, meaning they treat all the variables the same but some strategies may be more adventurous, meaning that they may venture further down the preference list. We further describe new techniques for discarding irrelevant instantiations which are crucial for the performance of these strategies in practice. These strategies are implemented in the SMT solver cvc5, where they contribute to the diversification of the solver's configuration space, as shown by our experimental results.

cs.AI↗

arXiv2019

Proceedings Sixth Workshop on Proof eXchange for Theorem Proving

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.

cs.LO↗

arXiv2019

CVC4SY for SyGuS-COMP 2019

CVC4Sy is a syntax-guided synthesis (SyGuS) solver based on bounded term enumeration and, for restricted fragments, quantifier elimination. The enumerative strategies are based on encoding term enumeration as an extension of the quantifier-free theory of algebraic datatypes and on a highly optimized brute-force algorithm. The quantifier elimination strategy extracts solutions from unsatisfiability proofs of the negated form of synthesis conjectures. It uses recent counterexample-guided techniques for quantifier instantiation that make finding such proofs practically feasible. CVC4Sy implements these strategies by extending the satisfiability modulo theories (SMT) solver CVC4. The strategy to be applied on a given problem is chosen heuristically based on the problem's structure. This document gives an overview of these techniques and their implementation in the SyGuS Solver CVC4Sy, an entry for SyGuS-Comp 2019.

cs.LO↗

arXiv2018

CVC4 at the SMT Competition 2018

This paper is a description of the CVC4 SMT solver as entered into the 2018 SMT Competition. We only list important differences from the 2017 SMT Competition version of CVC4. For further and more detailed information about CVC4, please refer to the original paper, the CVC4 website, or the source code on GitHub.

cs.LO↗

arXiv2017

Language and Proofs for Higher-Order SMT (Work in Progress)

Satisfiability modulo theories (SMT) solvers have throughout the years been able to cope with increasingly expressive formulas, from ground logics to full first-order logic modulo theories. Nevertheless, higher-order logic within SMT is still little explored. One main goal of the Matryoshka project, which started in March 2017, is to extend the reasoning capabilities of SMT solvers and other automatic provers beyond first-order logic. In this preliminary report, we report on an extension of the SMT-LIB language, the standard input format of SMT solvers, to handle higher-order constructs. We also discuss how to augment the proof format of the SMT solver veriT to accommodate these new constructs and the solving techniques they require.

cs.LO↗