Imagen de Portada

Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic (Extended Version)

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Niederhauser, Johannes, Brown, Chad E., Kaliszyk, Cezary
Formato:	Preprint
Publicado:	2024
Materias:	Logic in Computer Science
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

Experiments with Choice in Dependently-Typed Higher-Order Logic
por: Ranalter, Daniel, et al.
Publicado: (2024)

Hammering Higher Order Set Theory
por: Brown, Chad E., et al.
Publicado: (2025)

The Dependently Typed Higher-Order Form for the TPTP World
por: Ranalter, Daniel, et al.
Publicado: (2025)

Unification of Deterministic Higher-Order Patterns (Full Version)
por: Niederhauser, Johannes, et al.
Publicado: (2026)

Exploring Formal Math on the Blockchain: An Explorer for Proofgold
por: Brown, Chad E., et al.
Publicado: (2025)

Payment Channels with Proofs
por: Brown, Chad E., et al.
Publicado: (2025)

The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting (Full Version)
por: Niederhauser, Johannes, et al.
Publicado: (2025)

Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents
por: Brown, Chad E., et al.
Publicado: (2026)

Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers
por: Pąk, Karol, et al.
Publicado: (2024)

Differentiable Inductive Logic Programming in High-Dimensional Space
por: Purgał, Stanisław J., et al.
Publicado: (2022)

Polymorphism Meets DHOL
por: Ranalter, Rhea, et al.
Publicado: (2026)

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version)
por: Haselwarter, Philipp G., et al.
Publicado: (2026)

Partially Finite Model Reasoning in Description Logics Extended Version
por: Gogacz, Tomasz, et al.
Publicado: (2026)

Automated Strategy Invention for Confluence of Term Rewrite Systems
por: Zhang, Liao, et al.
Publicado: (2024)

A General Automata Model for First-Order Temporal Logics (Extended Version)
por: Geatti, Luca, et al.
Publicado: (2024)

Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System
por: Kura, Satoshi, et al.
Publicado: (2024)

Learning Guided Automated Reasoning: A Brief Survey
por: Blaauwbroek, Lasse, et al.
Publicado: (2024)

Left-Linear Completion with AC Axioms
por: Niederhauser, Johannes, et al.
Publicado: (2024)

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
por: Li, Kwing Hei, et al.
Publicado: (2025)

Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability
por: Bacci, Giorgio, et al.
Publicado: (2025)

Sharing and Linear Logic with Restricted Access (Extended Version)
por: Barenbaum, Pablo, et al.
Publicado: (2025)

Kuroda's Translation for Higher-Order Logic
por: Traversié, Thomas
Publicado: (2024)

Primitive Recursive Dependent Type Theory
por: Buchholtz, Ulrik, et al.
Publicado: (2024)

TableauxRocq: A Deep Embedding of Free-Variable Tableaux in Rocq
por: Rosain, Johann, et al.
Publicado: (2026)

Ordered Adjoint Logic (Extended Version)
por: Roshal, Sophia, et al.
Publicado: (2026)

First-Order LTLf Synthesis with Lookback (Extended Version)
por: Winkler, Sarah
Publicado: (2025)

Syntactic Effectful Realizability in Higher-Order Logic
por: Cohen, Liron, et al.
Publicado: (2025)

Mechanized Undecidability of Higher-order beta-Matching (Extended Version)
por: Dudenhefner, Andrej
Publicado: (2026)

Paraconsistent Semantics for Extended Fuzzy Logic Programs via Approximation Fixpoint Theory [Extended Version]
por: Kettmann, Pascal, et al.
Publicado: (2026)

Data-Aware Hybrid Tableaux
por: Areces, Carlos, et al.
Publicado: (2024)

Munkres' General Topology Autoformalized in Isabelle/HOL
por: Bryant, Dustin, et al.
Publicado: (2026)

Putting Perspective into OWL [sic]: Complexity-Neutral Standpoint Reasoning for Ontology Languages via Monodic S5 over Counting Two-Variable First-Order Logic (Extended Version with Appendix)
por: Álvarez, Lucía Gómez, et al.
Publicado: (2025)

Justification Logic for Intuitionistic Modal Logic (Extended Technical Report)
por: Marin, Sonia, et al.
Publicado: (2025)

Learning Rules Explaining Interactive Theorem Proving Tactic Prediction
por: Zhang, Liao, et al.
Publicado: (2024)

Non-Rigid Designators in Modal and Temporal Free Description Logics (Extended Version)
por: Artale, Alessandro, et al.
Publicado: (2024)

Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics (Extended Version)
por: Baader, Franz, et al.
Publicado: (2025)

Guarded Fragments Meet Dynamic Logic: The Story of Regular Guards (Extended Version)
por: Bednarczyk, Bartosz, et al.
Publicado: (2025)

Probabilistic Linear Logic Programming with an Application to Bayesian Network Computations (Extended Version)
por: Acclavio, Matteo, et al.
Publicado: (2026)

A Proof-Theoretic View of Basic Intuitionistic Conditional Logic (Extended Version)
por: Dalmonte, Tiziano, et al.
Publicado: (2025)

Extending Action Logic with Omega Iteration
por: Pshenitsyn, Tikhon
Publicado: (2025)