Publications


Publications in reverse chronological order | Publications ordered by theme | Current DBLP listing | Scholar Google | Arnetminer | Academic Search
To appear | 2022 | 2021 | 2020 | 2019 - 2015 | 2014 - 2010 | 2009 - 2005 | 2004 - 2000 | 1999 - 1995 | 1994 - 1991

To appear
International Patient Summary Terminology. Together with W. Del-Pinto, Y. Gao, G. Alghamdi, A. Lopez Osornio, and S. Roy (2023). MEDINFO 2023: Proceedings of the 19th World Congress on Medical and Health Informatics. Studies in Health Technology and Informatics, IOS Press.
Abstract, BiBTeX.
2022
Saturation-Based Uniform Interpolation for Multi-Agent Modal Logics. Together with R. Alassaf and U. Sattler. In D. Fernandez-Duque and A. Palmigiano and S. Pinchinat (eds), Advances in Modal Logic, Volume 14. College Publications, London, 37-58.
Abstract, BiBTeX, Proceedings.
Extracting Subontologies from SNOMED CT. Together with W. Del-Pinto and Y. Gao. In Groth, P. et al. (eds), The Semantic Web: ESWC 2022 Satellite Events. Lecture Notes in Computer Science, Vol. 13384, Springer, 291-294.
Abstract, BiBTeX, PDF, DOI link to Springer.
2021
Upwardly Abstracted Definition-Based Subontologies. Together with G. Alghamdi, W. Del-Pinto, and Y. Gao. In A. L. Gentile, and R. Goncalves (eds), K-CAP'21: Knowledge Capture Conference. ACM, 209-216.
Abstract, BiBTeX, DOI link to ACM.
Proceedings of the Second Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2021) associated with the 18th International Conference on Principles of Knowledge Representation and Reasoning (KR 2021). Together with C. Wernhard and Y. Zhao (eds) (2021). CEUR Workshop Proceedings, Vol. 3009, CEUR-WS.org.
Abstract, BiBTeX, Proceedings.
Proceedings of the 34th International Workshop on Description Logics (DL 2021). Together with M. Homola and V. Ryzhikov (eds) (2021) CEUR Workshop Proceedings, Vol. 2954, CEUR-WS.org.
Abstract, BiBTeX, Proceedings.
Tracking Semantic Evolutionary Changes in Large-Scale Ontological Knowledge Bases. Together with Z. Liu, C. Lu, G. Alghamdi and Y. Zhao. In G. Demartini, and G. Zuccon, and J. S. Culpepper, Z. Huang and H. Tong (eds), CIKM'21: The 30th ACM International Conference on Information and Knowledge Management. ACM, 1130-1139.
Abstract, BiBTeX, DOI link to ACM.
Semantic Forgetting in Expressive Description Logics. Together with M. Sakr. In B. Konev and G. Reger (eds), Frontiers of Combining Systems (FroCoS 2021). Lecture Notes in Computer Science, Vol. 12941, Springer, 118-136.
Abstract, BiBTeX, DOI link to Springer.
Concept Description and Definition Extraction for the ANEMONE System Together with D. Toluhi and B. Parsia. In Alechina, N. and Baldoni, M. and Logan, B. (eds), Engineering Multi-Agent Systems (EMAS 2021), Revised Selected Papers. Lecture Notes in Computer Science, Vol. 13190, Springer, Cham, 352-372.
Abstract, BiBTeX, PDF, DOI link to Springer.
2020
Signature-Based Abduction for Expressive Description Logics. Together with P. Koopmann, W. Del-Pinto, and S. Tourret. In Calvanese, D. and Erdem, E. (eds), Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning. AI Press.
Abstract, BiBTeX, PDF.
Deciding the Loosely Guarded Fragment and Querying Its Horn Fragment Using Resolution. Together with S. Zheng. In Proceedings of the Thirty-Fourth AAAI Conference on Artificial Intelligence (AAAI-2020). AAAI Press, 3080-3087.
Abstract, BiBTeX, PDF, DOI link to publisher.
A Practical Approach to Forgetting in Description Logics with Nominals. Together with Y. Zhao, Y. Wang, X. Zhang, H. Feng. In Proceedings of the Thirty-Fourth AAAI Conference on Artificial Intelligence (AAAI-2020). AAAI Press, 3073-3079.
Abstract, BiBTeX, PDF, DOI link to publisher.
Blocking and Other Enhancements for Bottom-Up Model Generation Methods Together with P. Baumgartner. Journal of Automated Reasoning 64 (2) 197-251.
Abstract, BiBTeX, Open access content sharing link from publisher.
2019
Ontology Extraction for Large Ontologies via Modularity and Forgetting. Together with J. Chen, G. Alghamdi, D. Walther and Y. Gao. In Kejriwal, M. and Szekely, P. A. and Troncy, R. (eds), Proceedings of the 10th International Conference on Knowledge Capture (K-CAP'19). ACM, 45-52.
Abstract, BiBTeX, PDF, DOI link to ACM.
Extending Forgetting-Based Abduction Using Nominals. Together with W. Del-Pinto. In A. Herzig and A. Popescu (eds), Proceedings of the 12th International Symposium on Frontiers of Combining Systems (FroCoS 2019). Lecture Notes in Artificial Intelligence, Vol. 11715, Springer, 185-202.
Abstract, BiBTeX, PDF, DOI link to Springer.
FAME(Q): An Automated Tool for Forgetting in Description Logics with Qualified Number Restrictions. Togther with Y. Zhao. In P. Fontaine (ed), Automated Deduction: CADE-27. Lecture Notes in Artificial Intelligence, Vol. 11716. Springer, 568-579.
Abstract, BiBTeX, PDF, DOI link to Springer.
ABox Abduction via Forgetting in ALC. Together with W. Del-Pinto. In P. van Hentenryck and Z.-H. Zhou (eds), Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence (AAAI-2019). AAAI Press, 2768-2775.
Abstract, BiBTeX, PDF, DOI link to publisher.
Tracking Logical Difference in Large-Scale Ontologies: A Forgetting-Based Approach. Together with Y. Zhao, G. Alghamdi, H. Feng, G. Stoilos, D. Juric and M. Khodadadi. In P. van Hentenryck and Z.-H. Zhou (eds), Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence (AAAI-2019). AAAI Press, 3116-3124.
Abstract, BiBTeX, PDF, DOI link to publisher.
Automating Automated Reasoning: The Case of Two Generic Automated Reasoning Tools Together with Y. Zohar, D. Tishkovsky and A. Zamansky. In Lutz, C., Sattler, U., Tinelli, C., Turhan, A.-Y. and Wolter, F. (eds), Description Logic, Theory Combination, and All That: Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, Vol. 11560, Springer, 610-638.
Abstract, BiBTeX, DOI link to Publisher.
Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF. Together with O. Beyersdorff, J., Blinkhorn, L., Chew and M. Suda. Journal of Automated Reasoning 63 (3) 597-623.
Abstract, BiBTeX, Open access DOI link.
2018
Methods and Metrics for Knowledge Base Engineering and Integration. Together with G. Stoilos, D. Geleta, S. Wartak, S. Hall, M. Khodadadi, Y. Zhao, and G. Alghamdi. In 9th Workshop on Ontology Design and Patterns (WOP 2018). CEUR Workshop Proceedings, Vol. 2195, CEUR-WS.org, 72-86.
Abstract, BiBTeX, PDF.
On Concept Forgetting in Description Logics with Qualified Number Restrictions. Together with Y. Zhao. In Lang, J. (ed), Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI 2018). AAAI Press/IJCAI, 1984-1990.
Abstract, BiBTeX, PDF, Details at publisher.
FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics. Together with Y. Zhao. In Galmiche, D. and Schulz, S. and Sebastiani, R. (eds), Automated Reasoning (IJCAR 2018). Lecture Notes in Artificial Intelligence, Volume 10900, Springer, 19-27.
Abstract, BiBTeX, PDF, DOI link to Springer.
2017
Automated Reasoning with Analytic Tableaux and Related Methods. The 26th International Conference, TABLEAUX 2017, Brasilia, Brazil, September 25-28, 2017, Proceedings. Together with C. Nalon (eds), Lecture Notes in Artificial Intelligence, Vol. 10501, Springer.
Abstract, BiBTeX, DOI Link.
Rule Refinement for Semantic Tableau Calculi. Together with D. Tishkovsky. In Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2017). Lecture Notes in Artificial Intelligence, Vol. 10501, Springer, 228-244.
Abstract, BiBTeX, PDF, (final version available via DOI link to Springer).
Role Forgetting for ALCOQH(top)-Ontologies Using an Ackermann Approach. Together with Y. Zhao. In Sierra, C. (ed), Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI 2017). AAAI Press/IJCAI, 1354-1361.
Abstract, BiBTeX, PDF.
2016
Blocking and Other Enhancements for Bottom-Up Model Generation Methods. Together with P. Baumgartner. arXiv e-Print 1611.09014 [cs.AI].
Abstract, BiBTeX, Full text via arXiv.
Forgetting Concept and Role Symbols in ALCOIH\mu+(top,and)-Ontologies. Together with Y. Zhao. In Kambhampati, S. (ed), Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence (IJCAI 2016). AAAI Press/IJCAI, 1345-1352.
Abstract, BiBTeX, PDF.
A Bi-Intuitionistic Modal Logic: Foundations and Automation. Together with J. G. Stell and D. Rydeheard. Journal of Logical and Algebraic Methods in Programming 85 (4), 500-519.
Abstract, BiBTeX, DOI Link to Elsevier.
Lifting QBF Resolution Calculi to DQBF. Together with O. Beyersdorff, L. Chew and M. Suda. In Creignou, N. and Le Berre, D. (eds), Theory and Applications of Satisfiability Testing (SAT 2016). Lecture Notes in Computer Science, Vol. 9710, Springer, 490-499.
Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
Forgetting Concept and Role Symbols in ALCOIH\mu+(top,and)-Ontologies. Together with Y. Zhao. In Lenzerini, M. and Penaloza, R. (eds), Proceedings of the 29th International Workshop on Description Logics (DL-2016). CEUR Workshop Proceedings, Vol. 1577, CEUR-WS.org.
Abstract, BiBTeX, PDF.
2015
Modal Tableau Systems with Blocking and Congruence Closure. Together with U. Waldmann. In De Nivelle, H. (eds), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2015). Lecture Notes in Computer Science, Vol. 9323, Springer, 38-53.
Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
Concept Forgetting in ALCOI-Ontologies Using an Ackermann Approach. Together with Y. Zhao. In Arenas et al (eds), The Semantic Web, 14th International Semantic Web Conference, ISWC 2015. Lecture Notes in Computer Science, Vol. 9366, Springer, 587-602.
Abstract, BiBTeX, PDF, (final version available via DOI link to Springer).
LETHE: A Saturation-Based Tool for Non-Classical Reasoning. Together with P. Koopmann. In Dumontier, et al (eds), Proceedings of the 4th International Workshop on OWL Reasoner Evaluation (ORE-2015). CEUR Workshop Proceedings, Vol. 1387, CEUR-WS.org.
Abstract, BiBTeX, PDF.
Concept Forgetting for ALCOI-Ontologies using an Ackermann Approach. Together with Y. Zhao. In Calvanese, D. and Konev, B. (eds), Proceedings of the 28th International Workshop on Description Logics (DL-2015). CEUR Workshop Proceedings, Vol. 1350, CEUR-WS.org.
Abstract, BiBTeX, PDF.
Saturation-Based Forgetting in the Description Logic SIF. Together with P. Koopmann. In Calvanese, D. and Konev, B. (eds), Proceedings of the 28th International Workshop on Description Logics (DL-2015). CEUR Workshop Proceedings, Vol. 1350, CEUR-WS.org.
Abstract, BiBTeX, PDF.
Uniform Interpolation and Forgetting for ALC Ontologies with ABoxes. Together with P. Koopmann. In Bonet, B. and Koenig, S. (eds), Proc. AAAI-2015. AAAI Press, 175-181.
Abstract, BiBTeX, PDF.
2014
Axiomatic and Tableau-Based Reasoning for Kt(H,R). Together with J. G. Stell and D. Rydeheard. In Goré, R. and Kurucz, A. (eds), Advances in Modal Logic, Volume 10. College Publications, London, 478-497,
Abstract, BiBTeX, PDF (final version available in the proceedings).
Forgetting and Uniform Interpolation of ALC-Ontologies with ABoxes. Together with P. Koopmann. In M. Bienvenu and R. Rosati (eds), Proceedings of the 27th International Workshop on Description Logics (DL-2014). CEUR Workshop Proceedings, Vol. 1193, CEUR-WS.org, 245-257.
Abstract, BiBTeX, PDF.
Terminating Minimal Model Generation Procedures for Propositional Modal Logics. Together with F. Papacchini. In S. Demri, D. Kapur, C. Weidenbach (eds), Automated Reasoning (IJCAR 2014). Lecture Notes in Artificial Intelligence, Vol. 8562, Springer, 381-395.
Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
Count and Forget: Uniform Interpolation of SHQ-Ontologies. Together with P. Koopmann. In S. Demri, D. Kapur, C. Weidenbach (eds), Automated Reasoning (IJCAR 2014). Lecture Notes in Artificial Intelligence, Vol. 8562, Springer, 434-448.
Abstract, BiBTeX, Long version (final version available via DOI link to Springer).
Tableau Development for a Bi-Intuitionistic Tense Logic. Together with J. G. Stell and D. Rydeheard. In Hofner, P., Jipsen, P., Kahl, W. and Müller, M. E. (eds), Relational and Algebraic Methods in Computer Science (RAMiCS 14). Lecture Notes in Computer Science, Vol. 8428, Springer, 412-428.
Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
Using Tableau to Decide Description Logics with Full Role Negation and Identity. Together with D. Tishkovsky. ACM Transactions on Computational Logic 15 (1).
Abstract, BiBTeX, DOI link to TOCL.
2013
Forgetting Concept and Role Symbols in ALCH-Ontologies. Together with P. Koopmann. In McMillan, K., Middeldorp, A. and Voronkov, A. (eds), Proc. LPAR 2013. Lecture Notes in Computer Science, Vol. 8312, Springer, 552-567.
Abstract, BiBTeX, PDF (final version will be available from Springer).
Implementation and Evaluation of Forgetting in ALC-Ontologies. Together with P. Koopmann. In Del Vescovo, C., Hahmann, T., Pearce, D. and Walther, D. (eds), Proceedings of the 7th International Workshop on Modular Ontologies (WoMo 2013). CEUR Workshop Proceedings, Vol. 1081, CEUR-WS.org, 1-12.
Abstract, BiBTeX, PDF, Electronic edition at CEUR-WS.org.
Frontiers of Combining Systems-FroCoS 2013. 9th International Symposium on Frontiers of Combining Systems, Nancy, September 18-20, 2013. Proceedings. Together with P. Fontaine and C. Ringeissen (eds). Lecture Notes in Artificial Intelligence, Vol. 8152, Springer.
Abstract, BiBTeX, DOI Link.
Uniform Interpolation of ALC-Ontologies Using Fixpoints. Together with P. Koopmann. In Fontaine, P. and Ringeissen, C. and Schmidt, R. A. (eds), Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013), Lecture Notes in Artificial Intelligence, Vol. 8152, Springer, 87-102.
Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
Computing Minimal Models Modulo Subset-Simulation for Propositional Modal Logics. Together with F. Papacchini. In Fontaine, P. and Ringeissen, C. and Schmidt, R. A. (eds), Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013), Lecture Notes in Artificial Intelligence, Vol. 8152, Springer, 279-294.
Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI. Together with M. Khodadadi and D. Tishkovsky. In Galmiche, D. and Larchey-Wendling, D. (eds), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2013). Lecture Notes in Computer Science, Vol. 8123 Springer, 188-202.
Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
Synthesising and Implementing Tableau Calculi for Interrogative Epistemic Logics. Together with S. Minica, M. Khodadadi and D. Tishkovsky. In Fontaine, P. and Schmidt, R. A. and Schulz, S. (eds), PAAR-2012: Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning. EPiC Series, Vol. 21 EasyChair, 109-123.
Abstract, BiBTeX, Link to EasyChair Proceedings.
MetTeL2: Towards a Tableau Prover Generation Platform. Together with D. Tishkovsky and M. Khodadadi. In Fontaine, P. and Schmidt, R. A. and Schulz, S. (eds), PAAR-2012: Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning. EPiC Series, Vol. 21 EasyChair, 149-162.
Abstract, BiBTeX, PDF, Link to EasyChair Proceedings.
PAAR-2012: Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning. Together with P. Fontaine and S. Schulz (eds). EPiC Series, Vol. 21, EasyChair.
Abstract, BiBTeX, Proceedings.
Refinement in the Tableau Synthesis Framework. Together with D. Tishkovsky. arXiv e-Print 1305.3131v1 [cs.LO].
Abstract, BiBTeX, arXiv Link.
First-Order Resolution Methods for Modal Logics. Together with U. Hustadt. In Voronkov, A. and Weidenbach, C. (eds), Programming Logics: Essays in Memory of Harald Ganzinger. Lecture Notes in Computer Science Vol. 7797, 345-391. Springer. Invited overview paper.
Abstract, BiBTeX, DOI.
Satisfiability Problem for Modal Logic with Global Counting Operators Coded in Binary is NExpTime-Complete. Together with M. Zawidzki and D. Tishkovsky. Information Processing Letters 113 (1-2) 34-38.
Abstract, BiBTeX, DOI.
2012
Labelled Tableaux for Temporal Logic with Cardinality Constraints. Together with C. Dixon, B. Konev, and D. Tishkovsky. Proceedings of the 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2012). IEEE Computer Society, 111-118.
Abstract, BiBTeX, DOI, PDF.
The Tableau Prover Generator MetTeL2. Together with D. Tishkovsky and M. Khodadadi. In del Cerro, L. F. and Herzig, A. and Mengin, J. (eds), Proceedings of the 13th European Conference on Logics in Artificial Intelligence (JELIA 2012). Lecture Notes in Computer Science Vol. 7519, Springer, 492-495.
Abstract, BiBTeX, PDF (final version available via DOI link to Springer).
Using Tableau to Decide Description Logics with Full Role Negation and Identity. Together with D. Tishkovsky. arXiv e-Print 1208.1476v1 [cs.LO].
Abstract, BiBTeX, arXiv Link.
An Abstract Tableau Calculus for the Description Logic SHOI Using Unrestricted Blocking and Rewriting. Together with M. Khodadadi and D. Tishkovsky. In Kazakov, Y. and Lembo, D. and Wolter, F. (eds), Proceedings of the 2012 International Workshop on Description Logics (DL-2012)., CEUR Workshop Proceedings 846, CEUR-WS.org.
Abstract, BiBTeX, PDF.
Proceedings of the 19th Automated Reasoning Workshop. Together with F. Papacchini (eds). Escholar uk-ac-man-scw:161817, The University of Manchester, UK.
Abstract, BiBTeX, Proceedings.
PAAR-2010: Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning. Together with B. Konev and S. Schulz (eds). EPiC Series, Vol. 9, EasyChair.
Abstract, BiBTeX, Proceedings.
A Comparison of Solvers for Propositional Dynamic Logic. Together with U. Hustadt. In Konev, B. and Schmidt, R. and Schulz, S. (eds), PAAR-2010: Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning. EPiC Series, Vol. 9, EasyChair, 63-73.
Abstract, BiBTeX, PDF.
The Ackermann Approach for Modal Logic, Correspondence Theory and Second-Order Reduction. Journal of Applied Logic 10 (1) 52-74.
Abstract, BiBTeX, DOI.
2011
A Tableau Calculus for Minimal Modal Model Generation. Together with F. Papacchini. Electronic Notes in Theoretical Computer Science 278 (3), 159-172.
Abstract, BiBTeX, DOI Link.
Special Issue of Selected Extended Papers of CADE-22. Together with Brigitte Pientka (eds). Journal of Automated Reasoning 47 (2) (2011).
BiBTeX, Editorial, Special issue.
MetTeL: A Tableau Prover with Logic-Independent Inference Engine. Together with D. Tishkovsky and M. Khodadadi. In Brunnler, K. and Metcalfe, G. (eds), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2011). Lecture Notes in Artificial Intelligence, Vol. 6793, Springer, 242-247.
Abstract, BiBTeX, DOI Link.
Automated Synthesis of Tableau Calculi. Together with D. Tishkovsky. Logical Methods in Computer Science 7 (2) 1-32,
Abstract, BiBTeX, Link to journal, arXiv Link.
Synthesising Terminating Tableau Calculi for Relational Logics: Invited Paper. In de Swart, H. (ed), Relational and Algebraic Methods in Computer Science (RAMiCS 12). Lecture Notes in Computer Science, Vol. 6663, Springer, 40-49.
Abstract, BiBTeX, DOI Link.
2010
Simulation and Synthesis of Deduction Calculi. Electronic Notes in Theoretical Computer Science 262, 221-229. Invited paper.
Abstract, BiBTeX, PDF, DOI Link.
A Tableau Method for Checking Rule Admissibility in S4. Together with S. Babenyshev, V. Rybakov and D. Tishkovsky. Electronic Notes in Theoretical Computer Science 262 17-32.
Abstract, BiBTeX, PDF, DOI Link.
Special issue on Practical Aspects of Automated Reasoning. Together with B. Konev and S. Schulz (eds). AI Communications 23 (2-3) 67-68.
BiBTeX, Editorial, Special issue.
2009
Reasoning Web: Semantic Technologies for Information Systems. 5th International Summer School 2009, Brixen-Bressanone, Italy, August 30-September 4, 2009, Tutorial Lectures. Together with Tessaris, S., Franconi, E., Eiter, Th., Gutierrez, C., Handschuh, S., Rousset, M.-C. (eds), Lecture Notes in Computer Science: Information Systems and Applications, incl. Internet/Web, and HCI, Vol. 5689, Springer.
Abstract, BiBTeX, DOI Link.
Automated Deduction-CADE-22. 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings. Schmidt, R. A. (ed), Lecture Notes in Artificial Intelligence, Vol. 5663, Springer.
Abstract, BiBTeX, DOI Link.
Automated Synthesis of Tableau Calculi. Together with D. Tishkovsky. In Giese, M. and Waaler, A. (eds), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2009). Lecture Notes in Computer Science, Vol. 5607, Springer, 310-324.
Abstract, BiBTeX, PDF, DOI Link.
A New Methodology for Developing Deduction Methods. In Annals of Mathematics and Artificial Intelligence 55 (1-2) 155-187.
Abstract, BiBTeX, PDF, DOI Link.
Special issue on Empirically Successful Computerized Reasoning. Together with G. Sutcliffe and S. Schulz (eds). Journal of Applied Logic 7 (1).
Abstract, BiBTeX, Link to JAL.
2008
Proceedings of the LPAR Workshops: Knowledge Exchange: Automated Provers and Proof Assistants, and The 7th International Workshop on the Implementation of Logics (KEAPPA & IWIL 2008). Together with Rudnicki, P., Sutcliffe, G., Konev, B., and Schulz, S. (eds), CEUR Workshop Proceedings, Vol. 418.
Abstract, BiBTeX, Full text via CEUR.
Improved Second-Order Quantifier Elimination in Modal Logic. In Hölldobler, S., Lutz, C. and Wansing, H. (eds), Proceedings of the 11th European Conference on Logics in Artificial Intelligence (JELIA). Lecture Notes in Computer Science, Vol. 5293, Springer, 375-388.
Abstract, BiBTeX, DOI Link.
Proceedings of the First International Workshop on Practical Aspects of Automated Reasoning (PAAR-2008/ESHOL-2008). Together with B. Konev and S. Schulz (eds). CEUR Workshop Proceedings, Vol. 373.
Abstract, BiBTeX, Full text via CEUR.
A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments. Together with D. Tishkovsky. In Armando, A., Baumgartner, P. and Dowek, G. (eds), Automated Reasoning (IJCAR 2008). Lecture Notes in Computer Science, Vol. 5195, Springer, 194-209.
Abstract, BiBTeX, DOI Link.
Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications. Together with D. M. Gabbay and A. Szalas. Studies in Logic: Mathematical Logic and Foundations, Vol. 12, College Publications.
Back-cover, BiBTeX, Publisher's info.
Order at amazon.co.uk, Order at amazon.com, Order at amazon.de.
Special issue on Relations and Kleene Algebras in Computer Science. Together with G. Struth (eds). Journal of Logic and Algebraic Programming 76 (1).
Abstract, BiBTeX, Link to JLAP.
On Combinations of Propositional Dynamic Logic and Doxastic Modal Logics. Together with D. Tishkovsky. Journal of Logic, Language and Information 17 (1) 109-129.
Abstract, BiBTeX, Full text via Springer.
2007
Using Tableau to Decide Expressive Description Logics with Role Negation. Together with D. Tishkovsky. In Aberer, K. et al (eds), The Semantic Web, 6th International Semantic Web Conference, 2nd Asian Semantic Web Conference, ISWC 2007 + ASWC 2007, Busan, Korea, November 11-15, 2007. Lecture Notes in Computer Science, Vol. 4825, Springer, 438-451.
Abstract, BiBTeX, DOI Link.
The Axiomatic Translation Principle for Modal Logic. Together with U. Hustadt. ACM Transactions on Computational Logic 8 (4) 1-55.
Abstract, BiBTeX, PDF, Final version at Elsevier via DOI Link.
System Description: SPASS Version 3.0. Together with C. Weidenbach, T. Hillenbrand, R. Rusev, and D. Topic. In Pfenning, F. (eds), Automated Deduction-CADE-21. Lecture Notes in Artificial Intelligence, Vol. 4603, Springer, 514-520.
Abstract, BiBTeX, PDF, DOI Link.
Deciding ALBO with Tableau. Together with D. Tishkovsky. In Calvanese, D., Franconi, E., Haarslev, V., Lembo, D., Motik, B., Tessaris, S., and Turhan, A. Y. (eds), Proceedings of the 20th International Workshop on Description Logics (DL-2007), Bozen-Bolzano University Press, 135-146.
Abstract, BiBTeX, PDF.
Computational Modal Logic. Together with I. Horrocks, U. Hustadt, and U. Sattler. In Blackburn, P. and van Benthem, J. and Wolter, F. (eds), Handbook of Modal Logic. Studies in Logic and Practical Reasoning, Volume 3, Elsevier, Amsterdam, 181-245. Commissioned overview paper.
Abstract, BiBTeX, Link to Elsevier.
2006
Investigating Finite Models of Non-Classical Logics with Relation Algebra and RelView. Together with R. Berghammer. In de Swart, H. and Orlowska, E. and Schmidt, G. and Roubens, M. (eds), Theory and Applications of Relational Structures as Knowledge Instruments II, Lecture Notes in Artficial intelligence Vol. 4342, Springer, 31-49.
Abstract, BiBTeX, PDF.
Developing Modal Tableaux and Resolution Methods via First-Order Resolution. In Governatori, G. and Hodkinson, I. and Venema, Y. (eds), Advances in Modal Logic, Volume 6. College Publications, London, 1-26. Invited paper.
Abstract, BiBTeX, PostScript.
Relations and Kleene Algebra in Computer Science: Proceedings of RelMiCS/AKA 2006. Schmidt, R. A. (ed), Lecture Notes in Computer Science, Vol. 4136, Springer.
Abstract, BiBTeX, DOI Link.
Blocking and Other Enhancements for Bottom-Up Model Generation Methods. Together with P. Baumgartner. In Furbach, U. and Shankar, N. (eds), Automated Reasoning: Third International Joint Conference on Automated Reasoning (IJCAR 2006). Lecture Notes in Artificial Intelligence, Vol. 4130, Springer, 125-139.
Abstract, BiBTeX, Full text via Springer.
Special issue on Implementation of Logics. Together with B. Konev and S. Schulz (eds). Journal of Applied Non-Classical Logic 16 (1-2).
Abstract, BiBTeX, Full text via JANCL.
Proceedings of the FLoC'06 Workshop on Empirically Successful Computerized Reasoning (ESCoR), 3rd International Joint Conference on Automated Reasoning. Together with G. Sutcliffe and S. Schulz (eds). CEUR Workshop Proceedings, Vol. 192.
Abstract, BiBTeX, Full text via CEUR.
Verification within the KARO Agent Theory. Together with U. Hustadt, C. Dixon, M. Fisher, J.-J. Meyer and W. van der Hoek. In C. Rouff, M. Hinchey, J. Rash, W. Truszkowski, and D. Gordon-Spears, editors, Agent Technology from a Formal Perspective, NASA Monographs in Systems and Software Engineering Series, Springer.
Abstract, BiBTeX, PDF.
2005
Advances in Modal Logic, Volume 5. Together with I. Pratt-Hartmann, M. Reynolds, and H. Wansing (eds). King's College Publications, London.
Abstract, BiBTeX, Online version.
Deciding Monodic Fragments by Temporal Resolution. Together with U. Hustadt and B. Konev. In Nieuwenhuis, R. (eds), Proceedings of the 20th International Conference on Automated Deduction (CADE-20), Lecture Notes in Artificial Intelligence, Vol. 3632, Springer, 204-218.
Abstract, BiBTeX, PDF, Full text via Springer.
2004
A Survey of Decidable First-Order Fragments and Description Logics. Together with U. Hustadt and L. Georgieva. Journal of Relational Methods in Computer Science 1, 251-276. Invited overview paper.
Abstract, BiBTeX, PostScript, PDF.
A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae. Together with U. Hustadt. Preprint Series CSPP-22, University of Manchester, UK.
Abstract, BiBTeX, PostScript, SpringerLink.
Interactions between Knowledge, Action and Commitment within Agent Dynamic Logic. Together with D. Tishkovsky and U. Hustadt. Studia Logica 78 (3), 381-415.
Abstract, BiBTeX, SpringerLink.
AiML-2004: Advances in Modal Logic. Together with I. Pratt-Hartmann, M. Reynolds and H. Wansing (eds). Technical Report UMCS-04-09-01, University of Manchester, UK.
Abstract, BiBTeX, PDF.
Multi-Agent Dynamic Logics with Informational Test. Together with D. Tishkovsky. Annals of Mathematics and Artificial Intelligence 42 (1-3), 5-36.
Abstract, BiBTeX, SpringerLink.
SCAN is complete for all Sahlqvist formulae. Together with V. Goranko, U. Hustadt, D. Vakarelov. In Berghammer, R., Möller, B. and Struth, G. (eds), Relational and Kleene-Algebraic Methods in Computer Science (RelMiCS 7). Lecture Notes in Computer Science Vol. 3051, Springer, 149-162.
Abstract, BiBTeX, PDF.
Two Proof Systems for Peirce Algebras. Together with E. Orlowska and U. Hustadt. In Berghammer, R. and Möller, B. and Struth, G. (eds), Relational and Kleene-Algebraic Methods in Computer Science (RelMiCS 7). Lecture Notes in Computer Science, Vol. 3051, Springer, 238-251.
Abstract, BiBTeX, Springer Link.
2003
Interaction between Knowledge, Action and Commitment within Agent Dynamic Logic Together with D. Tishkovsky and U. Hustadt. Preprint Series CSPP-27, University of Manchester, UK.
Abstract, BiBTeX, PostScript.
Mechanised Reasoning and Model Generation for Extended Modal Logics. Together with U. Hustadt. In de Swart, H. C. M. and Orlowska, E. and Schmidt, G. and Roubens, M. (eds), Theory and Applications of Relational Structures as Knowledge Instruments. Lecture Notes in Computer Science Vol. 2929, Springer, 38-67. Survey commissioned for the Kickoff Volume of COST Action 274.
Abstract, BiBTeX, PDF.
Fourth International Workshop on the Implementation of Logics. Together with B. Konev (eds). Technical Report ULCS-03-018, University of Liverpool.
Abstract, BiBTeX, PDF.
Combining Dynamic Logic with Doxastic Modal Logics. Together with D. Tishkovsky. In Balbiani, P. and Suzuki, N.-Y. and Wolter, F. and Zakharyaschev, M. (eds), Advances in Modal Logic, Volume 4. Chapter 18, King's College London Publications, 371-391.
Abstract, BiBTeX.
Hyperresolution for Guarded Formulae. Together with L. Georgieva and U. Hustadt. Journal of Symbolic Computation 36 (1-2), 163-192.
Abstract, ScienceDirect, BiBTeX.
A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae. Together with U. Hustadt. In Baader, F. (ed.), Automated Deduction-CADE-19. Lecture Notes in Artificial Intelligence Vol. 2741, Springer, 412-426.
Abstract, BiBTeX, PostScript.
2002
Logics with Commuting Action and Informational Modalities. Together with D. Tishkovsky. In Balbiani, P. and Suzuki, N.-Y. and Wolter, F. (eds), Advances in Modal Logic, Workshop Proceedings AiML'2002. 91-108.
Abstract, BiBTeX.
Multi-Agent Logic of Dynamic Belief and Knowledge. Together with D. Tishkovsky. In Flesca, S. and Greco, S. and Leone, N. and Ianni, G. (eds), Proceedings of the 8th European Conference on Logics in Artificial Intelligence (JELIA). Lecture Notes in Artificial Intelligence Vol. 2424, Springer, 38-49.
Abstract, BiBTeX, PostScript.
A New Clausal Class Decidable by Hyperresolution. Together with L. Georgieva and U. Hustadt. Preprint CSPP-18, Department of Computer Science, University of Manchester. Long version of a paper published in Proc. CADE'2002, LNAI, Springer.
Abstract, BiBTeX, PostScript.
On the Relationship Between Decidable Fragments, Non-Classical Logics, and Description Logics. Together with L. Georgieva and U. Hustadt. In Horrocks, I. and Tessaris, S. (eds), Proceedings of the 2002 International Workshop on Description Logics (DL'2002). CEUR Workshop Proceedings, Vol. CEUR-WS/Vol-53, 25-36.
Abstract, BiBTeX, PostScript.
On Axiomatic Products of PDL and S5: Substitution, Tests and Knowledge. Together with D. Tishkovsky. Bulletin of the Section of Logic 31 (1), 27-36.
BiBTeX, PostScript.
Scientific Benchmarking with Temporal Logic Decision Procedures. Together with U. Hustadt. In Fensel, D. and Giunchiglia, F. and McGuinness, D. and Williams, M.-A. (eds), Principles of Knowledge Representation and Reasoning: Proceedings of the Eighth International Conference (KR'2002). Morgan Kaufmann, 533-544.
Abstract, BiBTeX, PDF.
Using Resolution for Testing Modal Satisfiability and Building Models. Together with U. Hustadt. Journal of Automated Reasoning 28 (2) 205-232.
Abstract, BiBTeX, PostScript, DOI Link.
2001
Computational Space Efficiency and Minimal Model Generation for Guarded Formulae. Together with L. Georgieva and U. Hustadt. In R. Nieuwenhuis and A. Voronkov (eds), Logic for Programming, Artificial Intelligence, and Reasoning (Proc. LPAR'2001). Lecture Notes in Artificial Intelligence Vol. 2250, Springer, 85-99.
Abstract, BiBTeX, DOI Link.
Formulae which Highlight Differences between Temporal Logic and Dynamic Logic Provers. Together with U. Hustadt. In Giunchiglia, E. and Massacci, F. (eds), Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics. Technical Report DII 14/01, Dipartimento di Ingegneria dell'Informazione, Unversitä degli Studi di Siena, Siena, Italy, 68-76.
Abstract, BiBTeX, PostScript.
Reasoning about Agents in the KARO Framework. Together with U. Hustadt, C. Dixon, M. Fisher, J.-J. Meyer and W. van der Hoek. In Bettini, C. and Montanari, A. (eds), Proceedings of the Eighth International Symposium on Temporal Representation and Reasoning (TIME'2001). IEEE Computer Society, 206-213.
Abstract, BiBTeX.
Verification within the KARO Agent Theory. Together with U. Hustadt, C. Dixon, M. Fisher, J.-J. Meyer and W. van der Hoek. In Rash, J. L., Rouff, C. A., Truszkowski, W., Gordon, D. and Hinchey, M. G. (eds), Formal Approaches to Agent-Based Systems. Lecture Notes in Artificial Intelligence Vol. 1871, Springer, 33-47.
Abstract, BiBTeX.
A Resolution-Based Decision Procedure for Extensions of K4. Together with H. Ganzinger, U. Hustadt and C. Meyer. In Zakharyaschev, M. and Segerberg, K. and de Rijke, M. and Wansing, H. (eds), Advances in Modal Logic, Volume 2. Lecture Notes 119, CSLI Publications, Stanford, 225-246.
Abstract, BiBTeX, PostScript.
2000
Relational Grammars for Knowledge Representation. In Böttner, M. and Thümmel, W. (eds), Variable-Free Semantics. Artikulation und Sprache, Vol. 3, secolo Verlag, Osnabrück, Germany, 162-180.
Abstract, BiBTeX, PostScript.
MSPASS: Modal Reasoning by Translation and First-Order Resolution. Together with U. Hustadt. In Dyckhoff, R. (ed), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2000). Lecture Notes in Artificial Intelligence Vol. 1847, Springer, 67-71.
Abstract, BiBTeX, PostScript.
Hyperresolution for Guarded Formulae. Together with L. Georgieva and U. Hustadt. In Baumgartner, P. and Zhang, H. (eds), Proceedings of the Third International Workshop on First-Order Theorem Proving (FTP 2000). Fachberichte Informatik 5/2000, Institut für Informatik, Universität Koblenz-Landau, 101-112.
Abstract, BiBTeX, PostScript.
A Resolution Decision Procedure for Fluted Logic. Together with U. Hustadt. In McAllester, D. (ed), Automated Deduction-CADE-17. Lecture Notes in Artificial Intelligence Vol. 1831, Springer, 433-448.
Abstract, BiBTeX.
Resolution-Based Methods for Modal Logics. Together with H. de Nivelle and U. Hustadt. Logic Journal of the IGPL 8 (3) 265-292.
Abstract, BiBTeX, PostScript, Errata.
Normal Forms and Proofs in Combined Modal and Temporal Logics . Together with U. Hustadt, C. Dixon, and M. Fisher. In H. Kirchner and C. Ringeissen (eds), Proceedings of the International Workshop on Frontiers of Combining Systems (FroCoS'2000). Lecture Notes in Artificial Intelligence Vol. 1794, Springer, 73-87.
Abstract, BiBTeX, PostScript.
Using Resolution for Testing Modal Satisfiability and Building Models. Together with U. Hustadt. In Gent, I. P. and van Maaren, H. and Walsh, T. (eds), SAT 2000: Highlights of Satisfiability Research in the Year 2000. Frontiers in Artificial Intelligence and Applications 63, IOS Press, Amsterdam. Also in a special issue of Journal of Automated Reasoning.
Abstract, BiBTeX, PostScript.
Issues of Decidability for Description Logics in the Framework of Resolution. Together with U. Hustadt. In Caferra, R. and Salzer, G. (eds), Automated Deduction in Classical and Non-Classical Logic, Lecture Notes in Artificial Intelligence, Vol. 1761, Springer, 191-205.
Abstract, BiBTeX, PostScript.
1999
An Empirical Analysis of Modal Theorem Provers. Together with U. Hustadt. Journal of Applied Non-Classical Logics 9(4) 479-522.
Abstract, BiBTeX, PostScript.
MSPASS: Subsumption Testing with SPASS. Together with U. Hustadt and C. Weidenbach. In Lambrix, P. et al. (eds.), Proc. of Intern. Workshop on Description Logics'99, Linköping University, 136-137.
Abstract, BiBTeX, PostScript.
Decidability by Resolution for Propositional Modal Logics. Journal of Automated Reasoning 22(4), 379-396.
Abstract, BiBTeX, DOI Link.
On the Relation of Resolution and Tableaux Proof Systems for Description Logics. Together with U. Hustadt. In Dean, T. (ed), Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence (IJCAI'99). Vol. 1, Morgan Kaufmann, 110-115.
Abstract, BiBTeX, PDF.
Maslov's Class K Revisited. Together with U. Hustadt. In H. Ganzinger (ed.), Automated Deduction: CADE-16, Lecture Notes in Artificial Intelligence, Vol. 1632, Springer.
Abstract, BiBTeX, PostScript.
1998
Simplification and Backjumping in Modal Tableau. Together with U. Hustadt. In de Swart, H. (ed), Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX'98, Oisterwijk, The Netherlands, Proceedings. Lecture Notes in Computer Science Vol. 1397, Springer, 187-201.
Abstract, BiBTeX, PostScript.
Optimised Functional Translation and Resolution. Together with U. Hustadt and C. Weidenbach. In de Swart, H. (ed), Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX'98, Oisterwijk, The Netherlands, Proceedings. Lecture Notes in Computer Science Vol. 1397, Springer, 36-37. (Contribution to the comparison section of modal theorem provers).
Abstract, BiBTeX, PostScript.
Resolution is a Decision Procedure for Many Propositional Modal Logics. In Kracht, M., de Rijke, M., Wansing, H. and Zakharyaschev, M. (eds), Advances in Modal Logic, Volume 1, Lecture Notes 87, CSLI Publications, Stanford, 189-208.
Abstract, BiBTeX.
E-Unification for Subsystems of S4. In Nipkow, T. (ed.), Rewriting Techniques and Applications: 9th International Conference, RTA'98, Tsukuba, Japan, Proceedings, Lecture Notes in Computer Science Vol. 1379, Springer, 106-120.
Abstract, BiBTeX, PostScript.
Ordered E-Resolution and Path Logics. Manuscript. Submitted for publication.
Abstract, BiBTeX.
1997
Functional Translation and Second-Order Frame Properties of Modal Logics. Together with H.J. Ohlbach. Journal of Logic and Computation 7(5), 581-603.
Abstract, BiBTeX.
On Evaluating Decision Procedures for Modal Logics. Together with U. Hustadt. In Pollack, M. (ed), Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI'97), Vol. 1, Morgan Kaufmann, 202-207.
Abstract, BiBTeX.
Optimised Modal Translation and Resolution. PhD Thesis, Universität des Saarlandes, Saarbrücken, Germany.
Abstract, BiBTeX, PostScript (851KB).
Decidability by resolution for many modal logics. Extended abstract of a talk presented at ESSLLI'97, Aix-en-Provence, France.
Dvi.
On Evaluating Decision Procedures for Modal Logics. Together with U. Hustadt. Research Rep. MPI-I-97-2-003, MPI für Informatik, Saarbrücken.
Abstract, BiBTeX, PostScript.
Resolution is a Decision Procedure for Many Propositional Modal Logics. Research Rep. MPI-I-97-2-002, MPI für Informatik, Saarbrücken.
Abstract, BiBTeX, PostScript.
1996
Translating Graded Modalities into Predicate Logic. Together with H.J. Ohlbach and U.Hustadt. In H. Wansing (ed), Proof Theory for Modal Logic, Applied Logic Series 2, Kluwer, 253-291.
Abstract, BiBTeX.
1995
Symbolic Arithmetical Reasoning with Qualified Number Restrictions. Together with H.J. Ohlbach and U. Hustadt. In Proc. of Intern. Workshop on Description Logics'95 (held in Rome, 2-3 June 1995), Rap.07.95, Dipartimento di Informatica e Sistemistica, Univ. degli studia di Roma, 89-95.
Abstract, BiBTeX, PostScript
The Optimised Functional Translation and Graded Modal Logics. Together with H.J. Ohlbach. Combined abstract of talks held at the RelMiCs'96 Workshop in Parati, Brasil, 10-14 July.
Abstract, BiBTeX, DVI, PostScript
1994
Peirce Algebras. Together with C. Brink and K. Britz. Formal Aspects of Computing 6 (3), 339-358.
Abstract, BiBTeX, DVI, PostScript, DOI Link.
Peirce Algebras and Their Applications in Artificial Intelligence and Computational Linguistics: Abstract. SIGALA Newsletter 2 (1) 27. Abstract of a talk held at the Dagstuhl Seminar on Relational Methods in Computer Science, Dagstuhl, Germany (January 1994).
Abstract, BiBTeX, DVI, PostScript
Description Logics for Natural Language Processing. Together with D. Fehrer, U. Hustadt, M. Jaeger, A. Nonnengart, H.J. Ohlbach, Ch. Weidenbach and E. Weydert. In Proc. of Intern. Workshop on Description Logics'94, Document D-94-10, DFKI, Saarbrücken, 80-84.
Abstract, BiBTeX, PostScript
Terminological Logics and Conceptual Graphs: An Historical Perspective. Extended Abstract. In Kunze, J. and Stoyan, H. (eds), KI-94 Workshops: Extended Abstracts, Gesellschaft für Informatik, Bonn.
Abstract, BiBTeX, DVI, PostScript
Representations as Full Peirce algebras: Extended Abstract. Manuscript.
Abstract, BiBTeX
Existential Graphs for Terminological Logics. Manuscript.
Abstract, BiBTeX
Peirce Algebras and Relation Algebras are equipollent. Manuscript.
Abstract, BiBTeX
1993
Terminological Representation, Natural Language and Relation Algebra. In Ohlbach, H. J. (Ed.), Proc. of the sixteenth German AI Conf. (GWAI'92), Lecture Notes in Artificial Intelligence Vol. 671, Springer, Berlin, 357-371.
Abstract, BiBTeX, PostScript
Editorial: The possibility of generating true conjectures. Together with H. J. Ohlbach. Journal of Logic and Computation, 3(4), 341-343.
BiBTeX.
1992
Subsumption Computed Algebraically. Together with C. Brink. Computers and Mathematics with Applications 23 (2-9), Special edition on Semantic Networks in Artificial Intelligence, 329-342.
Abstract, BiBTeX, DOI Link.
MOTEL User Manual. Together with U. Hustadt A. Nonnengart and J. Timm. Tech. Rep. MPI-I-92-236, MPI für Informatik, Saarbrücken.
Abstract, BiBTeX, DVI, PostScript
1991
Autodescriptivity: Beware! Together with C. Brink and I.M. Rewitzky. The Computer Journal 34 (4), 380-381.
Abstract, BiBTeX, DOI Link.
Algebraic Terminological Representation. Tech. Rep. MPI-I-91-216, MPI für Informatik, Saarbrücken.
Abstract, BiBTeX, DVI, PostScript

Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 19 Feb 23
Copyright © 1996-2022 Renate A. Schmidt, School of Computer Science, Univ. Man., schmidt@cs.man.ac.uk