Labelled unit superposition calculi for instantiation-based reasoning

DOI10.1007/978-3-642-16242-8_33MaRDI QIDQ4933325zbMATH OpenOpenAlexFDO

Authors Konstantin Korovin, Christoph Sticksel

Publication date 12 October 2010

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-16242-8_33

Mathematics Subject Classification ID

Combined logics (03B62) Logic in artificial intelligence (68T27)

Recommendations

• Inst-Gen -- a modular approach to instantiation-based automated reasoning
• iProver-Eq: An Instantiation-Based Theorem Prover with Equality
• Computer Science Logic
• Labelled splitting
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)

Cited in

(3)

• SCL(EQ): SCL for first-order logic with equality
• Labelled Clauses
• Inst-Gen -- a modular approach to instantiation-based automated reasoning

This page was built for publication: Labelled unit superposition calculi for instantiation-based reasoning

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