×
Author ID: schmidt.renate-a Recent zbMATH articles by "Schmidt, Renate A."
Published as: Schmidt, Renate A.; Schmidt, Renate; Schmidt, R. A.; Schmidt, R.
Homepage: http://www.cs.man.ac.uk/~schmidt/
External Links: MGP

Publications by Year

Citations contained in zbMATH Open

67 Publications have been cited 373 times in 185 Documents Cited by Year
System description: Spass version 3.0. Zbl 1213.68577
Weidenbach, Christoph; Schmidt, Renate A.; Hillenbrand, Thomas; Rusev, Rostislav; Topic, Dalibor
26
2007
Second-order quantifier elimination. Foundations, computational aspects and applications. Zbl 1165.03011
Gabbay, Dov M.; Schmidt, Renate A.; Szałas, Andrzej
24
2008
Resolution-based methods for modal logics. Zbl 0947.03014
de Nivelle, Hans; Schmidt, Renate A.; Hustadt, Ullrich
18
2000
Blocking and other enhancements for bottom-up model generation methods. Zbl 1222.68357
Baumgartner, Peter; Schmidt, Renate A.
16
2006
MSPASS: Modal reasoning by translation and first-order resolution. Zbl 0963.68522
Hustadt, Ullrich; Schmidt, Renate A.
14
2000
Functional translation and second-order frame properties of modal logics. Zbl 0976.03019
Ohlbach, Hans Jürgen; Schmidt, Renate A.
13
1997
A principle for incorporating axioms into the first-order translation of modal formulae. Zbl 1278.03031
Schmidt, Renate A.; Hustadt, Ullrich
13
2003
Issues of decidability for description logics in the framework of resolution. Zbl 0955.03018
Hustadt, Ullrich; Schmidt, Renate A.
12
2000
Hyperresolution for guarded formulae. Zbl 1020.03007
Georgieva, Lilia; Hustadt, Ullrich; Schmidt, Renate A.
11
2003
A general tableau method for deciding description logics, modal logics and related first-order fragments. Zbl 1165.03319
Schmidt, Renate A.; Tishkovsky, Dmitry
10
2008
First-order resolution methods for modal logics. Zbl 1383.03031
Schmidt, Renate A.; Hustadt, Ullrich
9
2013
Using resolution for testing modal satisfiability and building models. Zbl 1005.03010
Hustadt, Ullrich; Schmidt, Renate A.
9
2002
A tableau method for checking rule admissibility in S4. Zbl 1345.03033
Babenyshev, Sergey; Rybakov, Vladimir; Schmidt, Renate A.; Tishkovsky, Dmitry
9
2010
Decidability by resolution for propositional modal logics. Zbl 0924.68178
Schmidt, Renate A.
8
1999
SCAN is complete for all Sahlqvist formulae. Zbl 1088.03019
Goranko, V.; Hustadt, U.; Schmidt, R. A.; Vakarelov, D.
8
2004
An empirical analysis of modal theorem provers. Zbl 1033.03501
Hustadt, Ullrich; Schmidt, Renate A.
7
1999
A new clausal class decidable by hyperresolution. Zbl 1072.68573
Georgieva, Lilia; Hustadt, Ullrich; Schmidt, Renate A.
7
2002
Peirce algebras. Zbl 0811.03047
Brink, Chris; Britz, Katarina; Schmidt, Renate A.
7
1994
Count and forget: uniform interpolation of \(\mathcal{SHQ}\)-ontologies. Zbl 1423.68482
Koopmann, Patrick; Schmidt, Renate A.
7
2014
Automated synthesis of tableau calculi. Zbl 1218.03012
Schmidt, Renate A.; Tishkovsky, Dmitry
7
2011
On combinations of propositional dynamic logic and doxastic modal logics. Zbl 1184.03012
Schmidt, Renate A.; Tishkovsky, Dmitry
6
2008
A bi-intuitionistic modal logic: foundations and automation. Zbl 1359.03018
Stell, John G.; Schmidt, Renate A.; Rydeheard, David
6
2016
The axiomatic translation principle for modal logic. Zbl 1367.03045
Schmidt, Renate A.; Hustadt, Ullrich
6
2007
A resolution decision procedure for fluted logic. Zbl 0963.03006
Schmidt, Renate A.; Hustadt, Ullrich
5
2000
A resolution-based decision procedure for extensions of K4. Zbl 0993.03017
Ganzinger, Harald; Hustadt, Ullrich; Meyer, Christoph; Schmidt, Renate A.
5
2001
Using tableau to decide description logics with full role negation and identity. Zbl 1287.03031
Schmidt, Renate A.; Tishkovsky, Dmitry
5
2014
A new methodology for developing deduction methods. Zbl 1192.68632
Schmidt, Renate A.
5
2009
Blocking and other enhancements for bottom-up model generation methods. Zbl 1468.68279
Baumgartner, Peter; Schmidt, Renate A.
4
2020
A refined tableau calculus with controlled blocking for the description logic \(\mathcal{SHOI}\). Zbl 1401.68307
Khodadadi, Mohammad; Schmidt, Renate A.; Tishkovsky, Dmitry
4
2013
Maslov’s class K revisited. Zbl 0937.03017
Hustadt, Ullrich; Schmidt, Renate A.
4
1999
Multi-agent dynamic logics with informational test. Zbl 1059.68131
Schmidt, Renate A.; Tishkovsky, Dmitry
4
2004
Interactions between knowledge, action and commitment within agent dynamic logic. Zbl 1077.03007
Schmidt, Renate A.; Tishkovsky, Dmitry; Hustadt, Ullrich
4
2004
Lifting QBF resolution calculi to DQBF. Zbl 1475.68431
Beyersdorff, Olaf; Chew, Leroy; Schmidt, Renate A.; Suda, Martin
4
2016
Computational space efficiency and minimal model generation for guarded formulae. Zbl 1275.68091
Georgieva, Lilia; Hustadt, Ullrich; Schmidt, Renate A.
4
2001
Automated synthesis of tableau calculi. Zbl 1218.03011
Schmidt, Renate A.; Tishkovsky, Dmitry
4
2009
Axiomatic and tableau-based reasoning for \(Kt (H, R)\). Zbl 1385.03026
Schmidt, Renate A.; Stell, John G.; Rydeheard, David
3
2014
Reinterpreting dependency schemes: soundness meets incompleteness in DQBF. Zbl 1468.03008
Beyersdorff, Olaf; Blinkhorn, Joshua; Chew, Leroy; Schmidt, Renate; Suda, Martin
3
2019
Subsumption computed algebraically. Zbl 0825.68604
Brink, Chris; Schmidt, Renate A.
3
1992
The Ackermann approach for modal logic, correspondence theory and second-order reduction. Zbl 1248.03039
Schmidt, Renate A.
3
2012
Mechanised reasoning and model generation for extended modal logics. Zbl 1203.03020
Schmidt, Renate A.; Hustadt, Ullrich
3
2003
Developing modal tableaux and resolution methods via first-order resolution. Zbl 1151.03013
Schmidt, Renate A.
3
2006
Using resolution for testing modal satisfiability and building models. Zbl 0984.03012
Hustadt, Ullrich; Schmidt, Renate A.
3
2000
\(E\)-unification for subsystems of \(S4\). Zbl 0903.03013
Schmidt, Renate A.
3
1998
Simplification and backjumping in modal tableau. Zbl 0909.03014
Hustadt, Ullrich; Schmidt, Renate A.
3
1998
Translating graded modalities into predicate logics. Zbl 0874.03021
Ohlbach, H. J.; Schmidt, R.; Hustadt, U.
3
1996
Verification within the KARO agent theory. Zbl 0988.68180
Hustadt, Ullrich; Dixon, Clare; Schmidt, Renate A.; Fisher, Michael; Meyer, John-Jules; van der Hoek, Wiebe
3
2001
Combining dynamic logic with doxastic modal logic. Zbl 1081.03023
Schmidt, Renate A.; Tishkovsky, Dmitry
3
2003
A tableau calculus for minimal modal model generation. Zbl 1347.03048
Papacchini, Fabio; Schmidt, Renate A.
3
2011
FAME: an automated tool for semantic forgetting in expressive description logics. Zbl 1511.68279
Zhao, Yizheng; Schmidt, Renate A.
2
2018
Automated deduction – CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2–7, 2009. Proceedings. Zbl 1167.68006
2
2009
Uniform interpolation of \(\mathcal{ALC}\)-ontologies using fixpoints. Zbl 1397.68163
Koopmann, Patrick; Schmidt, Renate A.
2
2013
Forgetting concept and role symbols in \(\mathcal{ALCH}\)-ontologies. Zbl 1407.68481
Koopmann, Patrick; Schmidt, Renate A.
2
2013
On axiomatic products of PDL and S5: Substitution, tests and knowledge. Zbl 1037.03032
Schmidt, Renate A.; Tishkovsky, Dmitry
2
2002
Normal forms and proofs in combined modal and temporal logics. Zbl 0964.03011
Hustadt, U.; Dixon, C.; Schmidt, R. A.; Fisher, M.
2
2000
Two proof systems for Peirce algebras. Zbl 1088.03056
Schmidt, Renate A.; Orłowska, Ewa; Hustadt, Ullrich
2
2004
Deciding monodic fragments by temporal resolution. Zbl 1135.03332
Hustadt, Ullrich; Konev, Boris; Schmidt, Renate A.
2
2005
Modal tableau systems with blocking and congruence closure. Zbl 1471.03018
Schmidt, Renate A.; Waldmann, Uwe
2
2015
Improved second-order quantifier elimination in modal logic. Zbl 1178.03033
Schmidt, Renate A.
2
2008
FAME(Q): an automated tool for forgetting in description logics with qualified number restrictions. Zbl 07178999
Zhao, Yizheng; Schmidt, Renate A.
1
2019
Computing minimal models modulo subset-simulation for modal logics. Zbl 1398.03095
Papacchini, Fabio; Schmidt, Renate A.
1
2013
Resolution is a decision procedure for many propositional modal logics. Zbl 0913.03019
Schmidt, Renate A.
1
1998
Relations and Kleene algebra in computer science. 9th international conference on relational methods in computer science and 4th international workshop on applications of Kleene algebra, RelMiCS/AKA 2006, Manchester, UK, August 29-September 2, 2006. Proceedings. Zbl 1134.68009
1
2006
Simulation and synthesis of deduction calculi. Zbl 1345.68254
Schmidt, Renate A.
1
2010
Tableau development for a bi-intuitionistic tense logic. Zbl 1345.03042
Stell, John G.; Schmidt, Renate A.; Rydeheard, David
1
2014
Multi-agent logics of dynamic belief and knowledge. Zbl 1013.68211
Schmidt, Renate A.; Tishkovsky, Dmitry
1
2002
MetTeL: a tableau prover with logic-independent inference engine. Zbl 1332.68205
Tishkovsky, Dmitry; Schmidt, Renate A.; Khodadadi, Mohammad
1
2011
Terminating minimal model generation procedures for propositional modal logics. Zbl 1423.68289
Papacchini, Fabio; Schmidt, Renate A.
1
2014
Blocking and other enhancements for bottom-up model generation methods. Zbl 1468.68279
Baumgartner, Peter; Schmidt, Renate A.
4
2020
Reinterpreting dependency schemes: soundness meets incompleteness in DQBF. Zbl 1468.03008
Beyersdorff, Olaf; Blinkhorn, Joshua; Chew, Leroy; Schmidt, Renate; Suda, Martin
3
2019
FAME(Q): an automated tool for forgetting in description logics with qualified number restrictions. Zbl 07178999
Zhao, Yizheng; Schmidt, Renate A.
1
2019
FAME: an automated tool for semantic forgetting in expressive description logics. Zbl 1511.68279
Zhao, Yizheng; Schmidt, Renate A.
2
2018
A bi-intuitionistic modal logic: foundations and automation. Zbl 1359.03018
Stell, John G.; Schmidt, Renate A.; Rydeheard, David
6
2016
Lifting QBF resolution calculi to DQBF. Zbl 1475.68431
Beyersdorff, Olaf; Chew, Leroy; Schmidt, Renate A.; Suda, Martin
4
2016
Modal tableau systems with blocking and congruence closure. Zbl 1471.03018
Schmidt, Renate A.; Waldmann, Uwe
2
2015
Count and forget: uniform interpolation of \(\mathcal{SHQ}\)-ontologies. Zbl 1423.68482
Koopmann, Patrick; Schmidt, Renate A.
7
2014
Using tableau to decide description logics with full role negation and identity. Zbl 1287.03031
Schmidt, Renate A.; Tishkovsky, Dmitry
5
2014
Axiomatic and tableau-based reasoning for \(Kt (H, R)\). Zbl 1385.03026
Schmidt, Renate A.; Stell, John G.; Rydeheard, David
3
2014
Tableau development for a bi-intuitionistic tense logic. Zbl 1345.03042
Stell, John G.; Schmidt, Renate A.; Rydeheard, David
1
2014
Terminating minimal model generation procedures for propositional modal logics. Zbl 1423.68289
Papacchini, Fabio; Schmidt, Renate A.
1
2014
First-order resolution methods for modal logics. Zbl 1383.03031
Schmidt, Renate A.; Hustadt, Ullrich
9
2013
A refined tableau calculus with controlled blocking for the description logic \(\mathcal{SHOI}\). Zbl 1401.68307
Khodadadi, Mohammad; Schmidt, Renate A.; Tishkovsky, Dmitry
4
2013
Uniform interpolation of \(\mathcal{ALC}\)-ontologies using fixpoints. Zbl 1397.68163
Koopmann, Patrick; Schmidt, Renate A.
2
2013
Forgetting concept and role symbols in \(\mathcal{ALCH}\)-ontologies. Zbl 1407.68481
Koopmann, Patrick; Schmidt, Renate A.
2
2013
Computing minimal models modulo subset-simulation for modal logics. Zbl 1398.03095
Papacchini, Fabio; Schmidt, Renate A.
1
2013
The Ackermann approach for modal logic, correspondence theory and second-order reduction. Zbl 1248.03039
Schmidt, Renate A.
3
2012
Automated synthesis of tableau calculi. Zbl 1218.03012
Schmidt, Renate A.; Tishkovsky, Dmitry
7
2011
A tableau calculus for minimal modal model generation. Zbl 1347.03048
Papacchini, Fabio; Schmidt, Renate A.
3
2011
MetTeL: a tableau prover with logic-independent inference engine. Zbl 1332.68205
Tishkovsky, Dmitry; Schmidt, Renate A.; Khodadadi, Mohammad
1
2011
A tableau method for checking rule admissibility in S4. Zbl 1345.03033
Babenyshev, Sergey; Rybakov, Vladimir; Schmidt, Renate A.; Tishkovsky, Dmitry
9
2010
Simulation and synthesis of deduction calculi. Zbl 1345.68254
Schmidt, Renate A.
1
2010
A new methodology for developing deduction methods. Zbl 1192.68632
Schmidt, Renate A.
5
2009
Automated synthesis of tableau calculi. Zbl 1218.03011
Schmidt, Renate A.; Tishkovsky, Dmitry
4
2009
Automated deduction – CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2–7, 2009. Proceedings. Zbl 1167.68006
2
2009
Second-order quantifier elimination. Foundations, computational aspects and applications. Zbl 1165.03011
Gabbay, Dov M.; Schmidt, Renate A.; Szałas, Andrzej
24
2008
A general tableau method for deciding description logics, modal logics and related first-order fragments. Zbl 1165.03319
Schmidt, Renate A.; Tishkovsky, Dmitry
10
2008
On combinations of propositional dynamic logic and doxastic modal logics. Zbl 1184.03012
Schmidt, Renate A.; Tishkovsky, Dmitry
6
2008
Improved second-order quantifier elimination in modal logic. Zbl 1178.03033
Schmidt, Renate A.
2
2008
System description: Spass version 3.0. Zbl 1213.68577
Weidenbach, Christoph; Schmidt, Renate A.; Hillenbrand, Thomas; Rusev, Rostislav; Topic, Dalibor
26
2007
The axiomatic translation principle for modal logic. Zbl 1367.03045
Schmidt, Renate A.; Hustadt, Ullrich
6
2007
Blocking and other enhancements for bottom-up model generation methods. Zbl 1222.68357
Baumgartner, Peter; Schmidt, Renate A.
16
2006
Developing modal tableaux and resolution methods via first-order resolution. Zbl 1151.03013
Schmidt, Renate A.
3
2006
Relations and Kleene algebra in computer science. 9th international conference on relational methods in computer science and 4th international workshop on applications of Kleene algebra, RelMiCS/AKA 2006, Manchester, UK, August 29-September 2, 2006. Proceedings. Zbl 1134.68009
1
2006
Deciding monodic fragments by temporal resolution. Zbl 1135.03332
Hustadt, Ullrich; Konev, Boris; Schmidt, Renate A.
2
2005
SCAN is complete for all Sahlqvist formulae. Zbl 1088.03019
Goranko, V.; Hustadt, U.; Schmidt, R. A.; Vakarelov, D.
8
2004
Multi-agent dynamic logics with informational test. Zbl 1059.68131
Schmidt, Renate A.; Tishkovsky, Dmitry
4
2004
Interactions between knowledge, action and commitment within agent dynamic logic. Zbl 1077.03007
Schmidt, Renate A.; Tishkovsky, Dmitry; Hustadt, Ullrich
4
2004
Two proof systems for Peirce algebras. Zbl 1088.03056
Schmidt, Renate A.; Orłowska, Ewa; Hustadt, Ullrich
2
2004
A principle for incorporating axioms into the first-order translation of modal formulae. Zbl 1278.03031
Schmidt, Renate A.; Hustadt, Ullrich
13
2003
Hyperresolution for guarded formulae. Zbl 1020.03007
Georgieva, Lilia; Hustadt, Ullrich; Schmidt, Renate A.
11
2003
Mechanised reasoning and model generation for extended modal logics. Zbl 1203.03020
Schmidt, Renate A.; Hustadt, Ullrich
3
2003
Combining dynamic logic with doxastic modal logic. Zbl 1081.03023
Schmidt, Renate A.; Tishkovsky, Dmitry
3
2003
Using resolution for testing modal satisfiability and building models. Zbl 1005.03010
Hustadt, Ullrich; Schmidt, Renate A.
9
2002
A new clausal class decidable by hyperresolution. Zbl 1072.68573
Georgieva, Lilia; Hustadt, Ullrich; Schmidt, Renate A.
7
2002
On axiomatic products of PDL and S5: Substitution, tests and knowledge. Zbl 1037.03032
Schmidt, Renate A.; Tishkovsky, Dmitry
2
2002
Multi-agent logics of dynamic belief and knowledge. Zbl 1013.68211
Schmidt, Renate A.; Tishkovsky, Dmitry
1
2002
A resolution-based decision procedure for extensions of K4. Zbl 0993.03017
Ganzinger, Harald; Hustadt, Ullrich; Meyer, Christoph; Schmidt, Renate A.
5
2001
Computational space efficiency and minimal model generation for guarded formulae. Zbl 1275.68091
Georgieva, Lilia; Hustadt, Ullrich; Schmidt, Renate A.
4
2001
Verification within the KARO agent theory. Zbl 0988.68180
Hustadt, Ullrich; Dixon, Clare; Schmidt, Renate A.; Fisher, Michael; Meyer, John-Jules; van der Hoek, Wiebe
3
2001
Resolution-based methods for modal logics. Zbl 0947.03014
de Nivelle, Hans; Schmidt, Renate A.; Hustadt, Ullrich
18
2000
MSPASS: Modal reasoning by translation and first-order resolution. Zbl 0963.68522
Hustadt, Ullrich; Schmidt, Renate A.
14
2000
Issues of decidability for description logics in the framework of resolution. Zbl 0955.03018
Hustadt, Ullrich; Schmidt, Renate A.
12
2000
A resolution decision procedure for fluted logic. Zbl 0963.03006
Schmidt, Renate A.; Hustadt, Ullrich
5
2000
Using resolution for testing modal satisfiability and building models. Zbl 0984.03012
Hustadt, Ullrich; Schmidt, Renate A.
3
2000
Normal forms and proofs in combined modal and temporal logics. Zbl 0964.03011
Hustadt, U.; Dixon, C.; Schmidt, R. A.; Fisher, M.
2
2000
Decidability by resolution for propositional modal logics. Zbl 0924.68178
Schmidt, Renate A.
8
1999
An empirical analysis of modal theorem provers. Zbl 1033.03501
Hustadt, Ullrich; Schmidt, Renate A.
7
1999
Maslov’s class K revisited. Zbl 0937.03017
Hustadt, Ullrich; Schmidt, Renate A.
4
1999
\(E\)-unification for subsystems of \(S4\). Zbl 0903.03013
Schmidt, Renate A.
3
1998
Simplification and backjumping in modal tableau. Zbl 0909.03014
Hustadt, Ullrich; Schmidt, Renate A.
3
1998
Resolution is a decision procedure for many propositional modal logics. Zbl 0913.03019
Schmidt, Renate A.
1
1998
Functional translation and second-order frame properties of modal logics. Zbl 0976.03019
Ohlbach, Hans Jürgen; Schmidt, Renate A.
13
1997
Translating graded modalities into predicate logics. Zbl 0874.03021
Ohlbach, H. J.; Schmidt, R.; Hustadt, U.
3
1996
Peirce algebras. Zbl 0811.03047
Brink, Chris; Britz, Katarina; Schmidt, Renate A.
7
1994
Subsumption computed algebraically. Zbl 0825.68604
Brink, Chris; Schmidt, Renate A.
3
1992
all top 5

Cited by 254 Authors

19 Schmidt, Renate A.
14 Hustadt, Ullrich
11 Dixon, Clare
7 Motik, Boris
7 Rybakov, Vladimir Vladimirovich
6 Baumgartner, Peter
6 Horrocks, Ian
5 Baader, Franz
5 Conradie, Willem
5 Szałas, Andrzej
5 Tishkovsky, Dmitry
5 Weidenbach, Christoph
4 Areces, Carlos
4 Benzmüller, Christoph Ewald
4 Beyersdorff, Olaf
4 Gabbay, Dov M.
4 Nalon, Cláudia
4 Papacchini, Fabio
4 Peltier, Nicolas
4 Stell, John G.
3 Balbiani, Philippe
3 Blinkhorn, Joshua
3 Demri, Stéphane P.
3 Georgatos, Konstantinos
3 Goranko, Valentin F.
3 Kapur, Deepak
3 Konev, Boris
3 Korovin, Konstantin
3 Palmigiano, Alessandra
3 Sofronie-Stokkermans, Viorica
3 Struth, Georg
3 Sutcliffe, Geoff
3 Voronkov, Andrei
3 Waldmann, Uwe
3 Wernhard, Christoph
3 Wolter, Frank
2 Alechina, Natasha
2 Babenyshev, Sergey
2 Bolotov, Alexander
2 Bonacina, Maria Paola
2 Borgwardt, Stefan
2 Botoeva, Elena
2 Brink, Chris
2 Britz, Katarina
2 Cialdea Mayer, Marta
2 Cuenca Grau, Bernardo
2 de Nivelle, Hans
2 de Rijke, Maarten
2 Furbach, Ulrich
2 Gencer, Çigdem
2 Golińska-Pilarek, Joanna
2 Gonçalves, Ricardo
2 Gorín, Daniel
2 Hella, Lauri T.
2 Höfner, Peter
2 Knorr, Matthias
2 Kohlhase, Michael
2 Koopmann, Patrick
2 Kovács, Laura Ildikó
2 Kutsia, Temur
2 Kuusisto, Antti
2 Leite, João
2 Mahajan, Meena
2 Orłowska, Ewa S.
2 Pelzer, Björn
2 Rabe, Florian
2 Ryzhikov, Vladislav
2 Sattler, Ulrike
2 Schon, Claudia
2 Sindoni, Giulia
2 Suda, Martin
2 Tinelli, Cesare
2 Tourret, Sophie
2 Vakarelov, Dimiter
2 Zakharyaschev, Michael Viktorovich
2 Zhang, Lan
1 Abate, Pietro
1 Alrabbaa, Christian
1 Artale, Alessandro
1 Avigad, Jeremy
1 Bártek, Filip
1 Benevides, Mario R. F.
1 Blackburn, Patrick
1 Böttner, Michael
1 Brown, Chad Edward
1 Cassano, Valentín
1 Castro, Pablo F.
1 Chen, Panfeng
1 Cheng, Che
1 Chew, Leroy
1 Claessen, Koen
1 Cucala, David Tena
1 Dachselt, Raimund
1 Danas, Ryan
1 Dastani, Mehdi M.
1 De Groot, Jim
1 de Moura, Leonardo
1 Dean, Edward T.
1 Degtyarev, Anatoli Ivanovich
1 Dix, Jurgen
...and 154 more Authors

Citations by Year