Image de couverture de livre

Non-Ground Congruence Closure

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Leidinger, Hendrik, Weidenbach, Christoph
Format:	Preprint
Publié:	2024
Sujets:	Logic in Computer Science I.2.3; F.3.1
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report
par: Klaus, Natalia, et autres
Publié: (2026)

Inductive First-Order Formula Synthesis by ASP: A Case Study in Invariant Inference
par: Yang, Ziyi, et autres
Publié: (2026)

Teaching Higher-Order Logic Using Isabelle
par: Lund, Simon Tobias, et autres
Publié: (2024)

Minimal Sequent Calculus for Teaching First-Order Logic: Lessons Learned
par: Villadsen, Jørgen
Publié: (2025)

ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings
par: Jana, Prithwish, et autres
Publié: (2025)

Mechanized HOL Reasoning in Set Theory
par: Guilloud, Simon, et autres
Publié: (2024)

Incomplete Descriptions and Qualified Definiteness
par: Więckowski, Bartosz
Publié: (2024)

Term Orders for Optimistic Lambda-Superposition
par: Bentkamp, Alexander, et autres
Publié: (2025)

Metric Equational Theories
par: Mardare, Radu, et autres
Publié: (2025)

Canonical for Automated Theorem Proving in Lean
par: Norman, Chase, et autres
Publié: (2025)

Implementing Dependent Type Theory Inhabitation and Unification
par: Norman, Chase, et autres
Publié: (2026)

OnlineProver: Experience with a Visualisation Tool for Teaching Formal Proofs
par: Perháč, Ján, et autres
Publié: (2025)

Discernment is all you need
par: Fuenmayor, David
Publié: (2026)

Taming Differentiable Logics with Coq Formalisation
par: Affeldt, Reynald, et autres
Publié: (2024)

SPARQL in N3: SPARQL CONSTRUCT as a rule language for the Semantic Web (Extended Version)
par: Arndt, Dörthe, et autres
Publié: (2025)

From Scientific Texts to Verifiable Code: Automating the Process with Transformers
par: Wang, Changjie, et autres
Publié: (2025)

A Coq-based Axiomatization of Tarski's Mereogeometry
par: Barlatier, Patrick, et autres
Publié: (2025)

Exponential Resolution Lower Bounds for Weak Pigeonhole Principle and Perfect Matching Formulas over Sparse Graphs
par: de Rezende, Susanna F., et autres
Publié: (2019)

Solving Quantified Modal Logic Problems by Translation to Classical Logics
par: Steen, Alexander, et autres
Publié: (2022)

A Sequent Calculus for General Inductive Definitions
par: Eede, Robbe Van den, et autres
Publié: (2026)

Complete Robust Hybrid Systems Reachability
par: Wafa, Noah Abou El, et autres
Publié: (2026)

Imandra CodeLogician: Neuro-Symbolic Reasoning for Precise Analysis of Software Logic
par: Lin, Hongyu, et autres
Publié: (2026)

Bidirectional Interpolation for the Lambda-Calculus -- Revisiting and Formalising Craig-Čubrić Interpolation
par: Bertrand, Meven Lennon, et autres
Publié: (2026)

Proving Cutoff Bounds for Safety Properties in First-Order Logic
par: Lotan, Raz, et autres
Publié: (2024)

Implicit Rankings for Verifying Liveness Properties in First-Order Logic
par: Lotan, Raz, et autres
Publié: (2024)

Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings
par: Lotan, Raz, et autres
Publié: (2026)

Unravelling Abstract Cyclic Proofs into Proofs by Induction
par: Grotenhuis, Lide, et autres
Publié: (2026)

Experiments with Choice in Dependently-Typed Higher-Order Logic
par: Ranalter, Daniel, et autres
Publié: (2024)

Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined Predicates
par: Echenim, Mnacho, et autres
Publié: (2023)

A Proof System with Causal Labels (Part II): checking Counterfactual Fairness
par: Ceragioli, Leonardo, et autres
Publié: (2025)

A Proof System with Causal Labels (Part I): checking Individual Fairness and Intersectionality
par: Ceragioli, Leonardo, et autres
Publié: (2025)

Calculational Design of Hyperlogics by Abstract Interpretation
par: Cousot, Patrick, et autres
Publié: (2024)

Safety, Relative Tightness and the Probabilistic Frame Rule
par: Jereb, Janez Ignacij, et autres
Publié: (2025)

Relation-Algebraic Verification of Disjoint-Set Forests
par: Guttmann, Walter
Publié: (2023)

Proof-Carrying Neuro-Symbolic Code
par: Komendantskaya, Ekaterina
Publié: (2025)

Approximate Axiomatization for Differentially-Defined Functions
par: Platzer, André, et autres
Publié: (2025)

Anthem 2.0: Automated Reasoning for Answer Set Programming
par: Fandinno, Jorge, et autres
Publié: (2025)

TPTP World Infrastructure for Non-classical Logics
par: Steen, Alexander, et autres
Publié: (2025)

Just Verification of Mutual Exclusion Algorithms with (Non-)Blocking and (Non-)Atomic Registers
par: van Glabbeek, Rob, et autres
Publié: (2026)

Separation Logic of Generic Resources via Sheafeology
par: van Starkenburg, Berend, et autres
Publié: (2025)