Ground joinability and connectedness in the superposition calculus

DOI10.1007/978-3-031-10769-6_11MaRDI QIDQ2104507zbMATH OpenOpenAlexFDO

Authors André Duarte, Konstantin Korovin

Publication date 7 December 2022

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-10769-6_11

zbMATH Keywords

closure redundancyconnectednessfirst-order theorem provingground joinabilitysuperposition

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A comprehensive framework for saturation theorem proving
• AC simplifications and closure redundancies in the superposition calculus
• An asymptotic equivalent for the number of total preorders on a finite set
• Basic paramodulation
• Critical pair criteria for completion
• Efficient encodings of first-order Horn formulas in equational logic
• Ground joinability and connectedness in the superposition calculus
• Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• Implementing Superposition in iProver (System Description)
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• MædMax: a maximal ordered completion tool
• On using ground joinable equations in equational theorem proving
• Ordered rewriting and confluence
• Paramodulation-based theorem proving
• Proving termination with multiset orderings
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• System description: E 1.8
• Term Rewriting and All That
• The CADE-14 ATP system competition
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• Twee: an equational theorem prover

Cited in

(9)

• A Galois connection approach to superposition and inaccessibility
• Ground joinability and connectedness in the superposition calculus
• The 11th IJCAR automated theorem proving system competition – CASC-J11
• Term ordering diagrams
• Partial redundancy in saturation
• Rewriting and inductive reasoning
• Saturating sorting without sorts
• On the (in-)completeness of destructive equality resolution in the superposition calculus
• Reducibility constraints in superposition

Describes a project that uses

Uses Software

• MadMax
• iProver
• Twee
• VAMPIRE
• Waldmeister
• TPTP
• E Theorem Prover

This page was built for publication: Ground joinability and connectedness in the superposition calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2104507)