Image de couverture de livre

TableauxRocq: A Deep Embedding of Free-Variable Tableaux in Rocq

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Rosain, Johann, Cailler, Julie
Format:	Preprint
Publié:	2026
Sujets:	Logic in Computer Science
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

TensorRocq: Enabling diagrammatic reasoning in Rocq
par: Caldwell, Benjamin, et autres
Publié: (2026)

Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP
par: Baudart, Guillaume, et autres
Publié: (2026)

String Diagrams for Monoidal Categories, in Rocq
par: Pous, Damien
Publié: (2026)

Revisiting the Fast Fourier Transform in Rocq
par: Théry, Laurent
Publié: (2022)

A Rocq Formalization of Monomial and Graded Orders
par: Boldo, Sylvie, et autres
Publié: (2025)

Nominal Sets in Rocq
par: Paranhos, Fabrício Sanches, et autres
Publié: (2025)

Adhesive category theory for graph rewriting in Rocq
par: Arsac, Samuel, et autres
Publié: (2025)

A Rocq Formalization of Simplicial Lagrange Finite Elements
par: Boldo, Sylvie, et autres
Publié: (2026)

RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation
par: Kozyrev, Andrei, et autres
Publié: (2025)

Data-Aware Hybrid Tableaux
par: Areces, Carlos, et autres
Publié: (2024)

A Curiously Effective Backtracking Strategy for Connection Tableaux
par: Färber, Michael
Publié: (2021)

SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus
par: Cailler, Julie, et autres
Publié: (2025)

Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic (Extended Version)
par: Niederhauser, Johannes, et autres
Publié: (2024)

RocqSmith: Can Automatic Optimization Forge Better Proof Agents?
par: Kozyrev, Andrei, et autres
Publié: (2026)

MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study
par: Viennot, Jules, et autres
Publié: (2025)

Tableaux for epistemic Gödel logic
par: Bílková, Marta, et autres
Publié: (2025)

Towards Term-based Verification of Diagrammatic Equivalence
par: Cailler, Julie, et autres
Publié: (2026)

Formal P-Category Theory and Normalization by Evaluation in Rocq
par: Berry, David G., et autres
Publié: (2025)

For Generalised Algebraic Theories, Two Sorts Are Enough
par: Avrillon, Samy, et autres
Publié: (2026)

Guiding Word Equation Solving using Graph Neural Networks (Extended Technical Report)
par: Abdulla, Parosh Aziz, et autres
Publié: (2024)

Universal Horn Sentences and the Joint Embedding Property
par: Bodirsky, Manuel, et autres
Publié: (2021)

Embedded Finite Models Beyond Restricted Quantifier Collapse
par: Benedikt, Michael, et autres
Publié: (2023)

Unification with Simple Variable Restrictions and Admissibility of $Π_{2}$-rules
par: Almeida, Rodrigo Nicolau, et autres
Publié: (2024)

Distribution-Free Normal Modal Logics
par: Hartonas, Chrysafis
Publié: (2024)

Normalisation for Negative Free Logics without and with Definite Descriptions
par: Kürbis, Nils
Publié: (2024)

Distribution-Free Modal Logics: Sahlqvist -- Van Benthem Correspondence
par: Chrysafis, et autres
Publié: (2025)

Variable binding and substitution for (nameless) dummies
par: Hirschowitz, André, et autres
Publié: (2022)

Strong Faithfulness for ELH Ontology Embeddings
par: Lacerda, Victor, et autres
Publié: (2023)

Fusions of One-Variable First-Order Modal Logics
par: Kontchakov, Roman, et autres
Publié: (2026)

On Knowledge Compilation For Two-Variable First-Order Logic
par: Meng, Qiaolan, et autres
Publié: (2026)

Variable Elimination as Rewriting in a Linear Lambda Calculus
par: Ehrhard, Thomas, et autres
Publié: (2025)

Two-Variable Logic for Hierarchically Partitioned and Ordered Data
par: Fiuk, Oskar, et autres
Publié: (2025)

About the Expressive Power and Complexity of Order-Invariance with Two Variables
par: Bednarczyk, Bartosz, et autres
Publié: (2023)

Generalization Problems with Atom-Variables in Languages with Binders and Equational Theories
par: Nantes-Sobrinho, Daniele, et autres
Publié: (2025)

The Complexity of Data-Free Nfer
par: Kauffman, Sean, et autres
Publié: (2024)

Trace Repair for Temporal Behavior Trees
par: Schirmer, Sebastian, et autres
Publié: (2025)

A Binary Quantifier for Definite Descriptions in Nelsonian Free Logic
par: Petrukhin, Yaroslav
Publié: (2024)

From Quantifier Depth to Quantifier Number: Separating Structures with k Variables
par: Vinall-Smeeth, Harry
Publié: (2023)

Words-to-Letters Valuations for Language Kleene Algebras with Variable and Constant Complements
par: Nakamura, Yoshiki, et autres
Publié: (2024)

Complexity of Weighted First-Order Model Counting in the Two-Variable Fragment with Counting Quantifiers: A Bound to Beat
par: Tóth, Jan, et autres
Publié: (2024)