Buchumschlag

Understanding and Improving Automated Proof Synthesis for Interactive Theorem Provers

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Zhang, Manqing, Dong, Yunwei, Zhou, Lingru, Xiao, Bingxu, Liu, Yepang
Format:	Preprint
Veröffentlicht:	2026
Schlagworte:	Logic in Computer Science 68Q60, 68T15, 03B35 D.2.4; F.3.1
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

Truth-Aware Decoding: A Program-Logic Approach to Factual Language Generation
von: Alpay, Faruk, et al.
Veröffentlicht: (2025)

A Logspace Constructive Proof of L=SL
von: Buss, Sam, et al.
Veröffentlicht: (2025)

Formalizing Pick's Theorem in Isabelle/HOL
von: Binder, Sage, et al.
Veröffentlicht: (2024)

Nominal techniques as an Agda library
von: Gabbay, Murdoch J., et al.
Veröffentlicht: (2026)

A declarative approach to specifying distributed algorithms using three-valued modal logic
von: Gabbay, Murdoch J., et al.
Veröffentlicht: (2025)

Declarative distributed algorithms as axiomatic theories in three-valued modal logic over semitopologies
von: Gabbay, Murdoch J.
Veröffentlicht: (2025)

Monitoring Hyperproperties over Observed and Constructed Traces
von: Chalupa, Marek, et al.
Veröffentlicht: (2025)

Proof-Carrying Certificates for LLM Pipelines: A Trust-Boundary Architecture
von: Koomullil, George
Veröffentlicht: (2026)

Simulating and model checking membrane systems using strategies in Maude
von: Rubio, Rubén, et al.
Veröffentlicht: (2024)

The complexity of being monitorable
von: Camerlo, Riccardo, et al.
Veröffentlicht: (2026)

The Solver's Paradox in Formal Problem Spaces
von: Rosko, Milan
Veröffentlicht: (2025)

Principal Types as Partial Involutions
von: Honsell, Furio, et al.
Veröffentlicht: (2024)

Domains, Information Frames, and Their Logic
von: Spreen, Dieter
Veröffentlicht: (2025)

From Gödel incompleteness to the consistency of circuit lower bounds
von: Atserias, Albert, et al.
Veröffentlicht: (2026)

A Qualitative Analysis of Kernel Extension for Higher Order Proof Checking
von: Wang, Shuai
Veröffentlicht: (2024)

Optimal Simultaneous Byzantine Agreement, Common Knowledge and Limited Information Exchange
von: van der Meyden, Ron
Veröffentlicht: (2025)

Matching logic -- a new axiomatization
von: Leuştean, Laurenţiu, et al.
Veröffentlicht: (2025)

Notes on applicative matching logic
von: Leuştean, Laurenţiu
Veröffentlicht: (2025)

Why the classes P and NP are not well-defined finitarily
von: Anand, Bhupinder Singh
Veröffentlicht: (2024)

Array-Carrying Symbolic Execution for Function Contract Generation
von: Lu, Weijie, et al.
Veröffentlicht: (2026)

Description Logics with Two Types of Definite Descriptions: Complexity, Expressiveness, and Automated Deduction
von: Sochański, Michał, et al.
Veröffentlicht: (2025)

Choiceless Polynomial Space
von: Ferrarotti, Flavio, et al.
Veröffentlicht: (2024)

Combining Mechanical and Agentic Specification Inference for Move
von: Grieskamp, Wolfgang, et al.
Veröffentlicht: (2026)

Arithmetics within the Linear Time Hierarchy
von: Pollett, Chris
Veröffentlicht: (2025)

NP-hard problems are not in BQP
von: Czerwinski, Reiner
Veröffentlicht: (2023)

Formally Verifying a Transformation from MLTL Formulas to Regular Expressions
von: Wang, Zili, et al.
Veröffentlicht: (2025)

Formalizing MLTL Formula Progression in Isabelle/HOL
von: Kosaian, Katherine, et al.
Veröffentlicht: (2024)

Locality, Consistency, and the Tractability Frontier
von: Simas, Tristan
Veröffentlicht: (2026)

QSeqSim: A Symbolic Simulator for Qiskit While Loops Using Sequential Quantum Circuits
von: Li, Zihao, et al.
Veröffentlicht: (2026)

Strategies, model checking and branching-time properties in Maude
von: Rubio, Rubén, et al.
Veröffentlicht: (2024)

Model checking strategy-controlled systems in rewriting logic
von: Rubio, Rubén, et al.
Veröffentlicht: (2024)

The Orientation Boundary for Step-Duplicating Recursors: Mechanized Impossibility, Escape, and Certification
von: Rahnama, Moses
Veröffentlicht: (2025)

Uniformity in learning structures
von: Cipriani, Vittorio, et al.
Veröffentlicht: (2025)

Classifying different criteria for learning algebraic structures
von: Bazhenov, Nikolay, et al.
Veröffentlicht: (2024)

A Modular Lean 4 Framework for Confluence and Strong Normalization of Lambda Calculi with Products and Sums
von: Ramos, Arthur, et al.
Veröffentlicht: (2025)

Proof-theoretic dilator and intermediate pointclasses
von: Jeon, Hanul
Veröffentlicht: (2025)

High-arity PAC learning via exchangeability
von: Coregliano, Leonardo N., et al.
Veröffentlicht: (2024)

A Constructive Proof of Rice's Theorem and the Halting Problem via Hilbert's Tenth Problem
von: Brossard, Jonathan
Veröffentlicht: (2026)

On Chaitin's Heuristic Principle and Halting Probability
von: Salehi, Saeed
Veröffentlicht: (2023)

On Woolhouse's Cotton-Spinning Problem
von: Groote, Jan Friso, et al.
Veröffentlicht: (2024)