Automated Synthesis of Tableau Calculi
This paper presents a method for synthesising sound and complete tableau calculi. Given a specification of the formal semantics of a logic, the method generates a set of tableau inference rules that can then be used to reason within the logic. The method guarantees that the generated rules form a ca...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2011-05-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/970/pdf |
| _version_ | 1797268706653372416 |
|---|---|
| author | Renate A. Schmidt Dmitry Tishkovsky |
| author_facet | Renate A. Schmidt Dmitry Tishkovsky |
| author_sort | Renate A. Schmidt |
| collection | DOAJ |
| description | This paper presents a method for synthesising sound and complete tableau
calculi. Given a specification of the formal semantics of a logic, the method
generates a set of tableau inference rules that can then be used to reason
within the logic. The method guarantees that the generated rules form a
calculus which is sound and constructively complete. If the logic can be shown
to admit finite filtration with respect to a well-defined first-order semantics
then adding a general blocking mechanism provides a terminating tableau
calculus. The process of generating tableau rules can be completely automated
and produces, together with the blocking mechanism, an automated procedure for
generating tableau decision procedures. For illustration we show the
workability of the approach for a description logic with transitive roles and
propositional intuitionistic logic. |
| first_indexed | 2024-04-25T01:36:45Z |
| format | Article |
| id | doaj.art-951f4f22bbec41e2a13e8edf104ad135 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:36:45Z |
| publishDate | 2011-05-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-951f4f22bbec41e2a13e8edf104ad1352024-03-08T09:15:48ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742011-05-01Volume 7, Issue 210.2168/LMCS-7(2:6)2011970Automated Synthesis of Tableau CalculiRenate A. Schmidthttps://orcid.org/0000-0002-6673-3333Dmitry TishkovskyThis paper presents a method for synthesising sound and complete tableau calculi. Given a specification of the formal semantics of a logic, the method generates a set of tableau inference rules that can then be used to reason within the logic. The method guarantees that the generated rules form a calculus which is sound and constructively complete. If the logic can be shown to admit finite filtration with respect to a well-defined first-order semantics then adding a general blocking mechanism provides a terminating tableau calculus. The process of generating tableau rules can be completely automated and produces, together with the blocking mechanism, an automated procedure for generating tableau decision procedures. For illustration we show the workability of the approach for a description logic with transitive roles and propositional intuitionistic logic.https://lmcs.episciences.org/970/pdfcomputer science - logic in computer sciencecomputer science - symbolic computationcs.sc |
| spellingShingle | Renate A. Schmidt Dmitry Tishkovsky Automated Synthesis of Tableau Calculi Logical Methods in Computer Science computer science - logic in computer science computer science - symbolic computation cs.sc |
| title | Automated Synthesis of Tableau Calculi |
| title_full | Automated Synthesis of Tableau Calculi |
| title_fullStr | Automated Synthesis of Tableau Calculi |
| title_full_unstemmed | Automated Synthesis of Tableau Calculi |
| title_short | Automated Synthesis of Tableau Calculi |
| title_sort | automated synthesis of tableau calculi |
| topic | computer science - logic in computer science computer science - symbolic computation cs.sc |
| url | https://lmcs.episciences.org/970/pdf |
| work_keys_str_mv | AT renateaschmidt automatedsynthesisoftableaucalculi AT dmitrytishkovsky automatedsynthesisoftableaucalculi |