Finding good proofs for description logic entailments using recursive quality measures

DOI10.1007/978-3-030-79876-5_17MaRDI QIDQ2055864zbMATH OpenOpenAlexFDO

Authors Christian Alrabbaa, Franz Baader, Stefan Borgwardt, Patrick Koopmann, Alisa Kovtunova

Publication date 1 December 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2104.13138

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• A proof theory for description logics.
• Essential structure of proofs as a measure of complexity
• Description Logic Reasoning in Prolog
• The complexity of theorem proving in circumscription and minimal entailment

Cites work

• An introduction to description logic
• Directed hypergraphs and applications
• Finding good proofs for description logic entailments using recursive quality measures
• scientific article; zbMATH DE number 4164180 (Why is no real title available?)
• Mechanizing Mathematical Reasoning
• Reconstructing proofs at the assertion level
• The incredible ELK. From polynomial procedures to efficient reasoning with \(\mathcal {EL}\) ontologies

Cited in

(8)

• Finding good proofs for description logic entailments using recursive quality measures
• Theorem proving as constraint solving with coherent logic
• Evonne: interactive proof visualization for description logics (system description)
• Efficiently explaining CSPs with unsatisfiable subset optimization
• The concrete \textsc{Evonne}: visualization meets concrete domain reasoning
• Small term reachability and related problems for terminating term rewriting systems
• On the complexity of the small term reachability problem for terminating term rewriting systems
• Explaining reasoning results for description logic ontologies (invited paper)

This page was built for publication: Finding good proofs for description logic entailments using recursive quality measures

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