000 02351nam a22004455i 4500
001 978-1-4471-4002-3
003 DE-He213
005 20170628033632.0
007 cr nn 008mamaa
008 120516s2012 xxk| s |||| 0|eng d
020 _a9781447140023
_9978-1-4471-4002-3
024 7 _a10.1007/978-1-4471-4002-3
_2doi
050 4 _aQA8.9-QA10.3
072 7 _aUYA
_2bicssc
072 7 _aMAT018000
_2bisacsh
072 7 _aCOM051010
_2bisacsh
082 0 4 _a005.131
_223
100 1 _aRademaker, Alexandre.
_eauthor.
245 1 2 _aA Proof Theory for Description Logics
_h[electronic resource] /
_cby Alexandre Rademaker.
264 1 _aLondon :
_bSpringer London :
_bImprint: Springer,
_c2012.
300 _aX, 106 p. 16 illus.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aSpringerBriefs in Computer Science,
_x2191-5768
505 0 _aIntroduction -- Background -- Sequent Calculus for ALC -- Comparing SCalc with other ALC Deduction Systems -- Natural Deduction for ALC.- A Proof Theory for ALCQI -- Proofs and Explanations -- A Prototype Theorem Prover -- Conclusion.
520 _aDescription Logics (DLs) is a family of formalisms used to represent knowledge of a domain. They are equipped with a formal logic-based semantics. Knowledge representation systems based on description logics provide various inference capabilities that deduce implicit knowledge from the explicitly represented knowledge. A Proof Theory for Description Logics introduces Sequent Calculi and Natural Deduction for some DLs (ALC, ALCQ). Cut-elimination and Normalization are proved for the calculi. The author argues that such systems can improve the extraction of computational content from DLs proofs for explanation purposes.
650 0 _aComputer science.
650 1 4 _aComputer Science.
650 2 4 _aMathematical Logic and Formal Languages.
650 2 4 _aMathematics of Computing.
710 2 _aSpringerLink (Online service)
773 0 _tSpringer eBooks
776 0 8 _iPrinted edition:
_z9781447140016
830 0 _aSpringerBriefs in Computer Science,
_x2191-5768
856 4 0 _uhttp://dx.doi.org/10.1007/978-1-4471-4002-3
912 _aZDB-2-SCS
999 _c16124
_d16124