Skip to main content
Erschienen in: Journal of Automated Reasoning 1/2020

12.02.2019

A Prover Dealing with Nominals, Binders, Transitivity and Relation Hierarchies

verfasst von: Marta Cialdea Mayer

Erschienen in: Journal of Automated Reasoning | Ausgabe 1/2020

Einloggen

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

This work describes the Sibyl prover, an implementation of a tableau based proof procedure for multi-modal hybrid logic with the converse, graded and global modalities, and enriched with features largely used in description logics: transitivity and relation hierarchies. The proof procedure is provably terminating when the input problem belongs to an expressive decidable fragment of hybrid logic. After a description of the implemented proof procedure, the way how the implementation deals with the most delicate aspects of the calculus is explained. Some experimental results, run on sets of randomly generated problems as well as some hand-tailored ones, show only a moderate deterioration in the performances of the prover when the number of transitivity and inclusion axioms increase. Sibyl is compared with other provers (HTab, the hybrid logic prover whose expressive power is closer to Sibyl’s one, and the first-order prover SPASS). The obtained results show that Sibyl has reasonable performances.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
1
Note that \(\textsf {HL}{\setminus } {\mathord \downarrow }\Box \) is a proper subset of \(\textsf {HL}{\setminus }\Box {\mathord \downarrow }\Box \).
 
2
Properly, the offspring relation and blockings are defined by mutual recursion on branch construction. The reader is referred to [13] for the details.
 
3
By default, (1) the equality rule and branch closure checks are applied with the highest priority. Following come (2) the @ rule, (3) the \(\textsf {A}\) rule, (4) the \(\wedge \) rule, (5) the \({\mathord \downarrow }\) rule, (6) the other universal rules, \(\Box \), \(\mathsf {Trans}\) and \(\mathsf {Link}\), (7) the blockable rules \(\Diamond \) and \(\textsf {E}\) and, finally, (8) the \(\vee \) rule.
 
4
Since hGen generated only formulae with forward relations, they were randomly replaced by the corresponding converse ones.
 
5
The first experiments with Sibyl, briefly reported in [14], used the same random test set described here. Unfortunately, in fact, hGen is no longer maintained, and could not be used to generate new problems.
 
6
The percentage of unsolved tests grows almost linearly from 0.2% in the test set with no assertions to 2.72% in the basic set.
 
7
Consider, for instance \(S_2\): the current state a is r-related, hence s-related, to exactly the two states \(a_1\) and \(a_2\) (from the first and second formulae); \(a_1\) is s-related (hence r-related) to neither \(a_1\) nor \(a_2\) (Formula 3), hence it must be r-related to some state b different from both \(a_1\) and \(a_2\). By transitivity, a is also r-related, hence s-related, to b, contradicting 2.
 
9
SPASS had already been used to test Sibyl for correctness, find out and correct bugs [14]. At that time, the language accepted by HTab was more restricted, since it did not include transitivity and relation inclusion assertions, and consequently HTab and Sibyl were not compared.
 
10
When called with a specific option, HLtranslate converts files from Sibyl input syntax to HTab one. The tool can be downloaded from Sibyl web page.
 
11
Moreover, the simplified translation of the global modalities given in Fig. 11 omits the trivial guards of the form \(x=x\) or \(y=y\).
 
12
It is fair to remark that for one of the 4860 considered problems HTab gives a “satisfiable” answer, while both Sibyl and SPASS declare it to be unsatisfiable. See also Sect. 6.3.2.
 
13
After preprocessing, the problem of size 2 without the relation inclusion assertions becomes \(S_2=\{\mathsf {Trans}(r),~\textsf {A}{\mathord \downarrow }x.\Diamond _r(p\wedge {\mathord \downarrow }y_0.x\mathord :\,\Diamond _r (p\wedge \lnot y_0), ~ \Box _r(a_1\vee a_2), ~a_1\mathord :\,(\lnot a_1\wedge \lnot a_2),~ a_2\mathord :\,(\lnot a_1\wedge \lnot a_2)\}\).
 
14
A node is a value of the main data type defined in the module Node, described later on.
 
15
Propositional letters and formulae of the form \(\Box _{R} F\) labelled by the nominal are stored in specific fields, so as to ease compatibility checks.
 
Literatur
1.
Zurück zum Zitat Areces, C., Blackburn, P., Marx, M.: A road-map on complexity for hybrid logics. In: Flum, J., Rodriguez-Artalejo, M. (eds.) Computer Science Logic, pp. 307–321. Springer (1999) Areces, C., Blackburn, P., Marx, M.: A road-map on complexity for hybrid logics. In: Flum, J., Rodriguez-Artalejo, M. (eds.) Computer Science Logic, pp. 307–321. Springer (1999)
2.
Zurück zum Zitat Areces, C., Gennari, R., Heguiabere, J., de Rijke, M.: Tree-based heuristics in modal theorem proving. In: Proceedings of the 14th European Conference on Artificial Intelligence (ECAI 2000), pp. 199–203 (2000) Areces, C., Gennari, R., Heguiabere, J., de Rijke, M.: Tree-based heuristics in modal theorem proving. In: Proceedings of the 14th European Conference on Artificial Intelligence (ECAI 2000), pp. 199–203 (2000)
3.
Zurück zum Zitat Areces, C., Gorín, D.: Unsorted functional translations. Electron. Notes Theor. Comput. Sci. 278, 3–16 (2011)MathSciNetCrossRef Areces, C., Gorín, D.: Unsorted functional translations. Electron. Notes Theor. Comput. Sci. 278, 3–16 (2011)MathSciNetCrossRef
4.
Zurück zum Zitat Areces, C., Heguiabehere, J.: Hylores 1.0: Direct resolution for hybrid logics. In: Proceedings of the 18th International Conference on Automated Deduction (CADE-18), pp. 156–160 (2002). Previously presented in the Proceedings of Methods for Modalities 2 (2001)CrossRef Areces, C., Heguiabehere, J.: Hylores 1.0: Direct resolution for hybrid logics. In: Proceedings of the 18th International Conference on Automated Deduction (CADE-18), pp. 156–160 (2002). Previously presented in the Proceedings of Methods for Modalities 2 (2001)CrossRef
5.
Zurück zum Zitat Areces, C., Heguiabehere, J.: hGen: A random CNF formula generator for hybrid languages. In: Proceedings of the 3rd Workshop on Methods for Modalities (M4M-3), Nancy, France (2003) Areces, C., Heguiabehere, J.: hGen: A random CNF formula generator for hybrid languages. In: Proceedings of the 3rd Workshop on Methods for Modalities (M4M-3), Nancy, France (2003)
6.
Zurück zum Zitat Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, P., Van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logics, pp. 821–868. Elsevier (2007) Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, P., Van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logics, pp. 821–868. Elsevier (2007)
7.
Zurück zum Zitat Balsiger, P., Heuerding, A., Schwendimann, S.: A benchmark method for the propositional modal logics K, KT, S4. J. Autom. Reason. 24(3), 297–317 (2000)MathSciNetCrossRef Balsiger, P., Heuerding, A., Schwendimann, S.: A benchmark method for the propositional modal logics K, KT, S4. J. Autom. Reason. 24(3), 297–317 (2000)MathSciNetCrossRef
9.
10.
Zurück zum Zitat Cerrito, S., Cialdea Mayer, M.: An efficient approach to nominal equalities in hybrid logic tableaux. J. Appl. Non-class. Log. 1–2(20), 39–61 (2010)MathSciNetCrossRef Cerrito, S., Cialdea Mayer, M.: An efficient approach to nominal equalities in hybrid logic tableaux. J. Appl. Non-class. Log. 1–2(20), 39–61 (2010)MathSciNetCrossRef
11.
Zurück zum Zitat Cerrito, S., Cialdea Mayer, M.: Nominal substitution at work with the global and converse modalities. In: Beklemishev, L., Goranko, V., Shehtman, V. (eds.) Advances in Modal Logic, vol. 8, pp. 57–74. College Publications (2010) Cerrito, S., Cialdea Mayer, M.: Nominal substitution at work with the global and converse modalities. In: Beklemishev, L., Goranko, V., Shehtman, V. (eds.) Advances in Modal Logic, vol. 8, pp. 57–74. College Publications (2010)
12.
Zurück zum Zitat Cerrito, S., Cialdea Mayer, M.: A tableaux based decision procedure for a broad class of hybrid formulae with binders. In: Automated Resoning with Analytic Tableaux and Related Methods (TABLEAUX 2011), vol. 6793 of LNAI, pp. 104–118. Springer (2011) Cerrito, S., Cialdea Mayer, M.: A tableaux based decision procedure for a broad class of hybrid formulae with binders. In: Automated Resoning with Analytic Tableaux and Related Methods (TABLEAUX 2011), vol. 6793 of LNAI, pp. 104–118. Springer (2011)
13.
Zurück zum Zitat Cerrito, S., Cialdea Mayer, M.: A tableau based decision procedure for a fragment of hybrid logic with binders, converse and global modalities. J. Autom. Reason. 51(2), 197–239 (2013)MathSciNetCrossRef Cerrito, S., Cialdea Mayer, M.: A tableau based decision procedure for a fragment of hybrid logic with binders, converse and global modalities. J. Autom. Reason. 51(2), 197–239 (2013)MathSciNetCrossRef
14.
Zurück zum Zitat Cialdea Mayer, M.: A proof procedure for hybrid logic with binders, transitivity and relation hierarchies. In: Proceedings of the 24th Conference on Automated Deduction (CADE-24), Number 7898 in LNCS, pp. 76–90. Springer (2013) Cialdea Mayer, M.: A proof procedure for hybrid logic with binders, transitivity and relation hierarchies. In: Proceedings of the 24th Conference on Automated Deduction (CADE-24), Number 7898 in LNCS, pp. 76–90. Springer (2013)
15.
Zurück zum Zitat Cialdea Mayer, M.: A proof procedure for hybrid logic with binders, transitivity and relation hierarchies (extended version). Technical report. arXiv:1312.2894 (2013) Cialdea Mayer, M.: A proof procedure for hybrid logic with binders, transitivity and relation hierarchies (extended version). Technical report. arXiv:​1312.​2894 (2013)
16.
Zurück zum Zitat Cialdea Mayer, M.: Extended decision procedure for a fragment of HL with binders. J. Autom. Reason. 53(3), 305–315 (2014)MathSciNetCrossRef Cialdea Mayer, M.: Extended decision procedure for a fragment of HL with binders. J. Autom. Reason. 53(3), 305–315 (2014)MathSciNetCrossRef
17.
Zurück zum Zitat Cialdea Mayer, M., Cerrito, S.: Herod and Pilate: two tableau provers for basic hybrid logic. In: Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010), pp. 255–262. Springer (2010) Cialdea Mayer, M., Cerrito, S.: Herod and Pilate: two tableau provers for basic hybrid logic. In: Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010), pp. 255–262. Springer (2010)
18.
Zurück zum Zitat Donini, F.M., Massacci, F.: EXPTIME tableaux for \(\cal{ALC}\). Artif. Intell. 124(1), 87–138 (2000)CrossRef Donini, F.M., Massacci, F.: EXPTIME tableaux for \(\cal{ALC}\). Artif. Intell. 124(1), 87–138 (2000)CrossRef
19.
Zurück zum Zitat Freeman, J.W.: Hard random 3-SAT problems and the Davis–Putnam procedure. Artif. Intell. 81(1), 183–198 (1996)MathSciNetCrossRef Freeman, J.W.: Hard random 3-SAT problems and the Davis–Putnam procedure. Artif. Intell. 81(1), 183–198 (1996)MathSciNetCrossRef
20.
Zurück zum Zitat Gent, I.P., Walsh, T.: The SAT phase transition. In: Proceedings of the Eleventh European Conference on Artificial Intelligence (ECAI’94), pp. 105–109 (1994) Gent, I.P., Walsh, T.: The SAT phase transition. In: Proceedings of the Eleventh European Conference on Artificial Intelligence (ECAI’94), pp. 105–109 (1994)
21.
Zurück zum Zitat Götzmann, D., Kaminski, M., Smolka, G.: Spartacus: a tableau prover for hybrid logic. Electron. Notes Theor. Comput. Sci. 262, 127–139 (2010). Proceedings of the 6th Workshop on Methods for Modalities (M4M-6 2009) Götzmann, D., Kaminski, M., Smolka, G.: Spartacus: a tableau prover for hybrid logic. Electron. Notes Theor. Comput. Sci. 262, 127–139 (2010). Proceedings of the 6th Workshop on Methods for Modalities (M4M-6 2009)
23.
Zurück zum Zitat Hladik, J.: Implementation and evaluation of a tableau algorithm for the guarded fragment. In: Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2002), pp. 145–159. Springer (2002) Hladik, J.: Implementation and evaluation of a tableau algorithm for the guarded fragment. In: Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2002), pp. 145–159. Springer (2002)
24.
Zurück zum Zitat Hoffmann, G.: Tâches de raisonnement en logiques hybrides. PhD thesis, Université Henri Poincaré—Nancy I (2010) Hoffmann, G.: Tâches de raisonnement en logiques hybrides. PhD thesis, Université Henri Poincaré—Nancy I (2010)
25.
Zurück zum Zitat Hoffmann, G., Areces, C.: HTab: A terminating tableaux system for hybrid logic. Electron. Notes Theor. Comput. Sci. 231, 3–19 (2007). Proceedings of the 5th Workshop on Methods for Modalities (M4M-5) Hoffmann, G., Areces, C.: HTab: A terminating tableaux system for hybrid logic. Electron. Notes Theor. Comput. Sci. 231, 3–19 (2007). Proceedings of the 5th Workshop on Methods for Modalities (M4M-5)
26.
Zurück zum Zitat Horrocks, I., Glimm, B., Sattler, U.: Hybrid logics and ontology languages. Electron. Notes Theor. Comput. Sci. 174, 3–14 (2007)CrossRef Horrocks, I., Glimm, B., Sattler, U.: Hybrid logics and ontology languages. Electron. Notes Theor. Comput. Sci. 174, 3–14 (2007)CrossRef
27.
Zurück zum Zitat Horrocks, I., Patel-Schneider, P.F.: Optimizing description logic subsumption. J. Log. Comput. 9, 267–293 (1999)MathSciNetCrossRef Horrocks, I., Patel-Schneider, P.F.: Optimizing description logic subsumption. J. Log. Comput. 9, 267–293 (1999)MathSciNetCrossRef
28.
Zurück zum Zitat Horrocks, I., Sattler, U.: A description logic with transitive and inverse roles and role hierarchies. J. Log. Comput. 9(3), 385–410 (1999)MathSciNetCrossRef Horrocks, I., Sattler, U.: A description logic with transitive and inverse roles and role hierarchies. J. Log. Comput. 9(3), 385–410 (1999)MathSciNetCrossRef
29.
Zurück zum Zitat Horrocks, I., Sattler, U.: A tableau decision procedure for \(\cal{SHOIQ}\). J. Autom. Reason. 39(3), 249–276 (2007)MathSciNetCrossRef Horrocks, I., Sattler, U.: A tableau decision procedure for \(\cal{SHOIQ}\). J. Autom. Reason. 39(3), 249–276 (2007)MathSciNetCrossRef
30.
Zurück zum Zitat Hustadt, U., Schmidt, R.A.: Simplification and backjumping in modaltableau. In: Automated Reasoning with Analytic Tableaux and RelatedMethods. TABLEAUX 1998, pp. 187–201. Springer, Berlin, Heidelberg (1998)MATH Hustadt, U., Schmidt, R.A.: Simplification and backjumping in modaltableau. In: Automated Reasoning with Analytic Tableaux and RelatedMethods. TABLEAUX 1998, pp. 187–201. Springer, Berlin, Heidelberg (1998)MATH
31.
Zurück zum Zitat Kaminski, M., Schneider, S., Smolka, G.: Terminating tableaux for graded hybrid logic with global modalities and role hierarchies. Log. Methods Comput. Sci. 7(1), 1–21 (2011)MathSciNetCrossRef Kaminski, M., Schneider, S., Smolka, G.: Terminating tableaux for graded hybrid logic with global modalities and role hierarchies. Log. Methods Comput. Sci. 7(1), 1–21 (2011)MathSciNetCrossRef
32.
Zurück zum Zitat Kaminski, M., Smolka, G.: Hybrid tableaux for the difference modality. Electron. Notes Theor. Comput. Sci. 231, 241–257 (2007). Proceedings of the 5th Workshop on Methods for Modalities (M4M-5) Kaminski, M., Smolka, G.: Hybrid tableaux for the difference modality. Electron. Notes Theor. Comput. Sci. 231, 241–257 (2007). Proceedings of the 5th Workshop on Methods for Modalities (M4M-5)
33.
Zurück zum Zitat Kaminski, M., Smolka, G.: Terminating tableau systems for hybrid logic with difference and converse. J. Log. Lang. Inf. 18(4), 437–464 (2009)MathSciNetCrossRef Kaminski, M., Smolka, G.: Terminating tableau systems for hybrid logic with difference and converse. J. Log. Lang. Inf. 18(4), 437–464 (2009)MathSciNetCrossRef
34.
Zurück zum Zitat Marx, M.: Narcissists, stepmothers and spies. In: Proceedings of the 2002 International Workshop on Description Logics (DL 2002). CEUR Workshop Proceedings, Vol. 53 (2002) Marx, M.: Narcissists, stepmothers and spies. In: Proceedings of the 2002 International Workshop on Description Logics (DL 2002). CEUR Workshop Proceedings, Vol. 53 (2002)
35.
Zurück zum Zitat Mundhenk, M., Schneider, T.: Undecidability of multi-modal hybrid logics. Electron. Notes Theor. Comput. Sci. 174(6), 29–43 (2007)CrossRef Mundhenk, M., Schneider, T.: Undecidability of multi-modal hybrid logics. Electron. Notes Theor. Comput. Sci. 174(6), 29–43 (2007)CrossRef
36.
Zurück zum Zitat Mundhenk, M., Schneider, T., Schwentick, T., Weber, V.: Complexity of hybrid logics over transitive frames. J. Appl. Log. 8(4), 422–440 (2010)MathSciNetCrossRef Mundhenk, M., Schneider, T., Schwentick, T., Weber, V.: Complexity of hybrid logics over transitive frames. J. Appl. Log. 8(4), 422–440 (2010)MathSciNetCrossRef
37.
Zurück zum Zitat Nalon, C., Hustadt, U., Dixon, C.: KSP: A resolution-based prover for multimodal K, Abridged Report. In: Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, pp. 4919–4923 (2017) Nalon, C., Hustadt, U., Dixon, C.: KSP: A resolution-based prover for multimodal K, Abridged Report. In: Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, pp. 4919–4923 (2017)
38.
Zurück zum Zitat Ohlbach, H., Schmidt, R.: Functional translation and second-order frame properties of modal logics. J. Log. Comput. 7(5), 581–603 (1997)MathSciNetCrossRef Ohlbach, H., Schmidt, R.: Functional translation and second-order frame properties of modal logics. J. Log. Comput. 7(5), 581–603 (1997)MathSciNetCrossRef
39.
Zurück zum Zitat Pelletier, F.J.: Seventy-five problems for testing automatic theorem provers. J. Autom. Reason. 2(2), 191–216 (1986)MathSciNetCrossRef Pelletier, F.J.: Seventy-five problems for testing automatic theorem provers. J. Autom. Reason. 2(2), 191–216 (1986)MathSciNetCrossRef
40.
Zurück zum Zitat Schild, K.: A correspondence theory for terminological logics: preliminary report. In: Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI-91), pp. 466–471 (1991) Schild, K.: A correspondence theory for terminological logics: preliminary report. In: Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI-91), pp. 466–471 (1991)
41.
Zurück zum Zitat Schmidt, R.A., Hustadt, U.: A principle for incorporating axioms into the first-order translation of modal formulae. In: Proceedings of the 19th International Conference on Automated Deduction (CADE-19), pp. 412–426 (2003)CrossRef Schmidt, R.A., Hustadt, U.: A principle for incorporating axioms into the first-order translation of modal formulae. In: Proceedings of the 19th International Conference on Automated Deduction (CADE-19), pp. 412–426 (2003)CrossRef
42.
Zurück zum Zitat Sutcliffe, G.: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. J. Autom. Reason. 59(4), 483–502 (2017)MathSciNetCrossRef Sutcliffe, G.: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. J. Autom. Reason. 59(4), 483–502 (2017)MathSciNetCrossRef
43.
Zurück zum Zitat ten Cate, B., Franceschet, M.: On the complexity of hybrid logics with binders. In: Proceedings of Computer Science Logic, pp. 339–354. Springer (2005) ten Cate, B., Franceschet, M.: On the complexity of hybrid logics with binders. In: Proceedings of Computer Science Logic, pp. 339–354. Springer (2005)
44.
Zurück zum Zitat Tsarkov, D., Horrocks, I., Patel-Schneider, P.F.: Optimizing terminological reasoning for expressive description logics. J. Autom. Reason. 39(3), 277–316 (2007)MathSciNetCrossRef Tsarkov, D., Horrocks, I., Patel-Schneider, P.F.: Optimizing terminological reasoning for expressive description logics. J. Autom. Reason. 39(3), 277–316 (2007)MathSciNetCrossRef
45.
Zurück zum Zitat van Eijck, J.: Constraint tableaux for hybrid logics. CWI, Amsterdam (2002) van Eijck, J.: Constraint tableaux for hybrid logics. CWI, Amsterdam (2002)
47.
Zurück zum Zitat Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Proceedings of the 22nd International Conference on Automated Deduction (CADE-22), pp. 140–145. Springer (2009) Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Proceedings of the 22nd International Conference on Automated Deduction (CADE-22), pp. 140–145. Springer (2009)
Metadaten
Titel
A Prover Dealing with Nominals, Binders, Transitivity and Relation Hierarchies
verfasst von
Marta Cialdea Mayer
Publikationsdatum
12.02.2019
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 1/2020
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-019-09513-3

Weitere Artikel der Ausgabe 1/2020

Journal of Automated Reasoning 1/2020 Zur Ausgabe