Ground joinability and connectedness in the superposition calculus
From MaRDI portal
Publication:2104507
DOI10.1007/978-3-031-10769-6_11OpenAlexW4289104029MaRDI QIDQ2104507
André Duarte, Konstantin Korovin
Publication date: 7 December 2022
Full work available at URL: https://doi.org/10.1007/978-3-031-10769-6_11
Related Items (2)
The 11th IJCAR automated theorem proving system competition – CASC-J11 ⋮ Ground joinability and connectedness in the superposition calculus
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Critical pair criteria for completion
- An asymptotic equivalent for the number of total preorders on a finite set
- The CADE-14 ATP system competition
- On using ground joinable equations in equational theorem proving
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- Efficient encodings of first-order Horn formulas in equational logic
- MædMax: a maximal ordered completion tool
- Basic paramodulation
- Twee: an equational theorem prover
- Ground joinability and connectedness in the superposition calculus
- Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
- AC simplifications and closure redundancies in the superposition calculus
- System Description: E 1.8
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- Proving termination with multiset orderings
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Term Rewriting and All That
- Implementing Superposition in iProver (System Description)
- A comprehensive framework for saturation theorem proving
- Ordered rewriting and confluence
This page was built for publication: Ground joinability and connectedness in the superposition calculus
