Manfred Schmidt-Schauß - Publications

[2018] Manfred Schmidt-Schauß and David Sabel. Nominal unification with atom and context variables. Frank report 59, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, January 2018.
bib | PDF ]
[2018] Manfred Schmidt-Schauß and Nils Dallmeyer. Space improvements and equivalences in a functional core language. In Horatiu Cirstea and David Sabel, editors, Proceedings Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation, Oxford, UK, 8th September 2017, volume 265 of Electronic Proceedings in Theoretical Computer Science, pages 98-112. Open Publishing Association, 2018.
bib | DOI ]
[2018] Manfred Schmidt-Schauß, David Sabel, and Yunus Kutz. Nominal unification with atom-variables. Journal of Symbolic Computation, 2018.
bib | DOI ]
[2017] Manfred Schmidt-Schauß, David Sabel, and Nils Dallmeyer. Improvements for concurrent haskell with futures. Frank report 58, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, December 2017.
bib | PDF ]
[2017] Manfred Schmidt-Schauß and Nils Dallmeyer. Space improvements and equivalences in a polymorphically typed functional core language: Context lemmas and proofs. Frank report 57, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, July 2017.
bib | PDF ]
[2017] Nils Dallmeyer and Manfred Schmidt-Schauß. An environment for analyzing space optimizations in call-by-need functional languages. In Horatiu Cirstea and Santiago Escobar, editors, Proceedings Third International Workshop on Rewriting Techniques for Program Transformations and Evaluation, Porto, Portugal, 23rd June 2016, volume 235 of Electronic Proceedings in Theoretical Computer Science, pages 78-92. Open Publishing Association, 2017.
bib | DOI ]
[2017] Manfred Schmidt-Schauß and David Sabel. Improvements in a call-by-need functional core language: Common subexpression elimination and resource preserving translations. Science of Computer Programming, 147:3-26, 2017.
bib | DOI | PDF | http ]
[2017] Markus Lohrey and Manfred Schmidt-Schauß. Processing succinct matrices and vectors. Theory Comput. Syst., 61(2):322-351, 2017.
bib | DOI | arXiv version | http ]
[2016] Manfred Schmidt-Schauß and David Sabel. Unification of program expressions with recursive bindings. In Germán Vidal, editor, PPDP '16: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, pages 160-173, New York, NY, USA, September 2016. ACM. ©ACM.
bib | DOI | PDF | http ]
[2016] Manfred Schmidt-Schauß and David Sabel. Improvements in a functional core language with call-by-need operational semantics. Frank report 55, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, August 2016.
bib | PDF | previous version (2.0) | previous version (1.0) ]
[2016] Manfred Schmidt-Schauß and David Sabel. Sharing decorations for improvements in a functional core language with call-by-need operational semantics. Frank report 56, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, February 2016.
bib | PDF | previous version (2.0) | previous version (1.0) ]
[2016] David Sabel and Manfred Schmidt-Schauß. A call-by-need lambda calculus with scoped work decorations. In Wolf Zimmermann, Lukas Alperowitz, Bernd Brügge, Jörn Fahsel, Andrea Herrmann, Anne Hoffmann, Andreas Krall, Dieter Landes, Horst Lichter, Dirk Riehle, Ina Schaefer, Constantin Scheuermann, Alexander Schlaefer, Sibylle Schupp, Andreas Seitz, Andreas Steffens, André Stollenwerk, and Rüdiger Weißbach, editors, Software Engineering Workshops 2016, volume 1559 of CEUR Workshop Proceedings, pages 70-90. CEUR-WS.org, February 2016. 9. Arbeitstagung Programmiersprachen (ATPS'16).
bib | PDF ]
[2016] Manfred Schmidt-Schauß, Temur Kutsia, Jordi Levy, and Mateu Villaret. Nominal unification of higher order expressions with recursive let. In Manuel V. Hermenegildo and Pedro López-García, editors, Logic-Based Program Synthesis and Transformation - 26th International Symposium, LOPSTR 2016, Edinburgh, UK, September 6-8, 2016, Revised Selected Papers, volume 10184 of Lecture Notes in Computer Science, pages 328-344, 2016.
bib | DOI | http ]
[2015] Manfred Schmidt-Schauß and David Sabel. Sharing-aware improvements in a call-by-need functional core language. In Ralf Lämmel, editor, Proceedings of the 27th Symposium on the Implementation and Application of Functional Programming Languages, IFL '15, pages 6:1-6:12, New York, NY, USA, September 2015. ACM.
bib | DOI | PDF | http ]
[2015] David Sabel and Manfred Schmidt-Schauß. Observing Success in the Pi-Calculus. In Yuki Chiba, Santiago Escobar, Naoki Nishida, David Sabel, and Manfred Schmidt-Schauß, editors, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015), volume 46 of OpenAccess Series in Informatics (OASIcs), pages 31-46, Dagstuhl, Germany, July 2015. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.
bib | DOI | http ]
[2015] Yuki Chiba, Santiago Escobar, Naoki Nishida, David Sabel, and Manfred Schmidt-Schauß, editors. 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2015, July 2, 2015, Warsaw, Poland, volume 46 of OASIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, July 2015.
bib | http ]
[2015] Manfred Schmidt-Schauß and David Sabel. Improvements in a functional core language with call-by-need operational semantics. In Moreno Falaschi and Elvira Albert, editors, Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, Siena, Italy, July 14-16, 2015, pages 220-231. ACM, July 2015.
bib | DOI | PDF | http ]
[2015] Manfred Schmidt-Schauß, David Sabel, Joachim Niehren, and Jan Schwinghammer. Observational program calculi and the correctness of translations. Theoretical Computer Science, 577:98-124, 2015. ©Elsevier B.V.,.
bib | DOI | PDF | http ]
[2015] Manfred Schmidt-Schauß, David Sabel, and Elena Machkasova. Simulation in the call-by-need lambda-calculus with letrec, case, constructors, and seq. Logical Methods in Computer Science, 11(1), 2015.
bib | DOI | PDF | http ]
[2015] Adria Gascón, Ashish Tiwari, and Manfred Schmidt-Schauß. One context unification problems solvable in polynomial time. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 499-510. IEEE, 2015.
bib | DOI | http ]
[2015] Adria Gascón, Manfred Schmidt-Schauß, and Ashish Tiwari. Two-restricted one context unification is in polynomial time. In Stephan Kreutzer, editor, 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany, volume 41 of LIPIcs, pages 405-422. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015.
bib | DOI | http ]
[2014] Manfred Schmidt-Schauß and David Sabel. Applicative may- and should-simulation in the call-by-value lambda calculus with amb. In Gilles Dowek, editor, Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8560 of Lecture Notes in Computer Science, pages 379-394. Springer, July 2014. ©Springer Verlag, The original publication is available at www.springerlink.com.
bib | DOI ]
[2014] Manfred Schmidt-Schauß. Concurrent programming languages and methods for semantic analyses (extended abstract of invited talk). In Gilles Dowek, editor, Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8560 of Lecture Notes in Computer Science, pages 21-30. Springer, July 2014. ©Springer Verlag, The original publication is available at www.springerlink.com.
bib | DOI | slides (RTA/TLCA 2014) ]
[2014] Manfred Schmidt-Schauß and David Sabel. Contextual equivalences in call-by-need and call-by-name polymorphically typed calculi (preliminary report). In Manfred Schmidt-Schauß, Masahiko Sakai, David Sabel, and Yuki Chiba, editors, First International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2014, July 13, 2014, Vienna, Austria, volume 40 of OASICS, pages 63-74. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, July 2014.
bib | DOI | slides (WPTE 2014) ]
[2014] Manfred Schmidt-Schauß, Masahiko Sakai, David Sabel, and Yuki Chiba, editors. First International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2014, July 13, 2014, Vienna, Austria, volume 40 of OASICS. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, July 2014.
bib | http ]
[2014] Markus Lohrey and Manfred Schmidt-Schauß. Processing succinct matrices and vectors. In Edward A. Hirsch, Sergei O. Kuznetsov, Jean-Éric Pin, and Nikolay K. Vereshchagin, editors, Computer Science - Theory and Applications - 9th International Computer Science Symposium in Russia, CSR 2014, Moscow, Russia, June 7-11, 2014. Proceedings, volume 8476 of Lecture Notes in Computer Science, pages 245-258. Springer, June 2014. ©Springer Verlag, The original publication is available at www.springerlink.com.
bib | arXiv version | http ]
[2014] Manfred Schmidt-Schauß and David Sabel. Applicative may- and should-simulation in the call-by-value lambda calculus with amb. Frank report 54, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, April 2014.
bib | PDF ]
[2014] David Sabel and Manfred Schmidt-Schauß. Contextual equivalence for the pi-calculus that can stop. Frank report 53, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, March 2014.
bib | PDF ]
[2013] Manfred Schmidt-Schauß and David Sabel. Correctness of an STM Haskell implementation. In Greg Morrisett and Tarmo Uustalu, editors, Proceedings of the 18th ACM SIGPLAN International Conference on Functional programming, ICFP '13, pages 161-172, New York, NY, USA, September 2013. ACM.
bib | DOI | PDF | http ]
[2013] Manfred Schmidt-Schauß, David Sabel, and Elena Machkasova. Simulation in the call-by-need lambda-calculus with letrec, case, constructors, and seq. Frank report 49, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, August 2013.
bib | PDF | previous version ]
[2013] Manfred Schmidt-Schauß, Elena Machkasova, and David Sabel. Extending abramsky's lazy lambda calculus: (non)-conservativity of embeddings. Frank report 51, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, August 2013.
bib | PDF | previous version ]
[2013] Manfred Schmidt-Schauß, Elena Machkasova, and David Sabel. Extending Abramsky's Lazy Lambda Calculus: (Non)-Conservativity of Embeddings. In Femke van Raamsdonk, editor, 24th International Conference on Rewriting Techniques and Applications (RTA 2013), volume 21 of Leibniz International Proceedings in Informatics (LIPIcs), pages 239-254, Dagstuhl, Germany, June 2013. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.
bib | DOI | PDF | http ]
[2013] Manfred Schmidt-Schauß, Conrad Rau, and David Sabel. Algorithms for Extended Alpha-Equivalence and Complexity. In Femke van Raamsdonk, editor, 24th International Conference on Rewriting Techniques and Applications (RTA 2013), volume 21 of Leibniz International Proceedings in Informatics (LIPIcs), pages 255-270, Dagstuhl, Germany, June 2013. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.
bib | DOI | PDF | http ]
[2013] Manfred Schmidt-Schauß, David Sabel, Joachim Niehren, and Jan Schwinghammer. Observational program calculi and the correctness of translations. Frank report 52, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, May 2013.
bib | PDF ]
[2013] Manfred Schmidt-Schauß and David Sabel. Correctness of an STM Haskell implementation. Frank report 50, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, March 2013.
bib | PDF | previous version (1.0) ]
[2013] David Sabel and Manfred Schmidt-Schauß. A two-valued logic for properties of strict functional programs allowing partial functions. Journal of Automated Reasoning, 50(4):383-421, 2013. ©Springer Verlag, The original publication is available at www.springerlink.com.
bib | DOI | PDF | http ]
[2013] Manfred Schmidt-Schauß. Linear compressed pattern matching for polynomial rewriting (extended abstract). In Rachid Echahed and Detlef Plump, editors, Proceedings 7th International Workshop on Computing with Terms and Graphs, volume 110 of EPTCS, pages 29-40, 2013.
bib | http ]
[2012] Manfred Schmidt-Schauß. Matching of compressed patterns with character-variables. In Ashish Tiwari, editor, 23. RTA 2012, volume 15 of LIPIcs, pages 272-287. Dagstuhl Publishing, Saarbrücken/Wadern, June 2012.
bib | PDF | http ]
[2012] David Sabel and Manfred Schmidt-Schauß. Conservative concurrency in Haskell. In Nachum Dershowitz, editor, Proceedings of the 27th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2012), 25-28 June 2012, Dubrovnik, Croatia, pages 561-570, June 2012. ©IEEE.
bib | PDF ]
[2012] Conrad Rau, David Sabel, and Manfred Schmidt-Schauß. Correctness of program transformations as a termination problem. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, Automated Reasoning - Proceedings of the 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012, volume 7364 of Lecture Notes in Computer Science, pages 462-476. Springer Berlin / Heidelberg, June 2012. ©Springer Verlag, The original publication is available at www.springerlink.com.
bib | PDF ]
[2012] David Sabel and Manfred Schmidt-Schauß. On conservativity of Concurrent Haskell. Frank report 47, Institut für Informatik, Goethe-Universität Frankfurt am Main, April 2012.
bib | PDF | previous version ]
[2012] Conrad Rau, David Sabel, and Manfred Schmidt-Schauß. Encoding induction in correctness proofs of program transformations as a termination problem. In Georg Moser, editor, 12th International Workshop on Termination, WST 2012, February 19-23, 2012, Obergurgl, Austria, pages 74-78, February 2012. Published online and open access by G. Moser, Institute of Computer Science, University of Innsbruck, Austria.
bib | Online Proceedings | PDF ]
[2012] Manfred Schmidt-Schauß and Georg Schnitger. Fast equality test for straight-line compressed strings. Information Processing Letters, 112(8-9):341-345, 2012.
bib | DOI | http ]
[2012] Markus Lohrey, Sebastian Maneth, and Manfred Schmidt-Schauß. Parameter reduction and automata evaluation for grammar-compressed trees. J. Comput. Syst. Sci., 78(5):1651-1669, 2012.
bib | http ]
[2011] Manfred Schmidt-Schauß, David Sabel, and Altug Anis. Congruence closure of compressed terms in polynomial time. In Cesare Tinelli and Viorica Sofronie-Stokkermans, editors, Frontiers of Combining Systems, volume 6989 of Lecture Notes in Computer Science, pages 227-242. Springer Berlin / Heidelberg, October 2011. ©Springer Verlag, The original publication is available at www.springerlink.com.
bib | PDF | http ]
[2011] Conrad Rau and Manfred Schmidt-Schauß. Computing overlappings by unification in the deterministic lambda calculus lr with letrec, case, constructors, seq and variable chains. Frank report 46, Institut für Informatik. Fachbereich Informatik und Mathematik. Goethe-Universität Frankfurt am Main, August 2011.
bib | PDF ]
[2011] Manfred Schmidt-Schauß, David Sabel, and Elena Machkasova. Counterexamples to applicative simulation and extensionality in non-deterministic call-by-need lambda-calculi with letrec. Information Processing Letters, 111(14):711-716, July 2011.
bib | DOI | http ]
[2011] Adrià Gascón, Guillem Godoy, and Manfred Schmidt-Schauß. Unification and matching on compressed terms. ACM Transactions on Computational Logic (TOCL), 12:26:1-26:37, July 2011.
bib | DOI | PDF | http ]
[2011] David Sabel and Manfred Schmidt-Schauß. A contextual semantics for concurrent haskell with futures. In Proceedings of the 13th international ACM SIGPLAN symposium on Principles and practices of declarative programming, PPDP '11, pages 101-112, New York, NY, USA, July 2011. ACM. ©ACM, 2011.
bib | DOI | PDF | http ]
[2011] Conrad Rau and Manfred Schmidt-Schauß. A unification algorithm to compute overlaps in a call-by-need lambda-calculus with variable-binding chains. In Proceedings of the 25th International Workshop on Unification, pages 35-41, July 2011.
bib | PDF | http ]
[2011] Manfred Schmidt-Schauß and Georg Schnitger. Fast equality test for straight-line compressed strings. Frank report 45, Institut für Informatik, Goethe-Universität Frankfurt am Main, April 2011.
bib | PDF ]
[2011] David Sabel and Manfred Schmidt-Schauß. A contextual semantics for Concurrent Haskell with futures. Frank report 44, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, March 2011.
bib | PDF ]
[2011] Manfred Schmidt-Schauß. Pattern matching of compressed terms and contexts and polynomial rewriting. Frank report 43, Institut für Informatik. Goethe-Universität Frankfurt am Main, February 2011.
bib | PDF ]
[2011] David Sabel and Manfred Schmidt-Schauß. Reconstruction of a logic for inductive proofs of properties of functional programs. Frank report 39, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, January 2011.
bib | PDF | previous version (3.0) | previous version (2.0) | previous version (1.0) ]
[2011] Jordi Levy, Manfred Schmidt-Schauß, and Mateu Villaret. On the complexity of bounded second-order unification and stratified context unification. Logic Journal of the IGPL, 19(6):763-789, 2011.
bib | PDF ]
[2011] Conrad Rau and Manfred Schmidt-Schauß. Towards correctness of program transformations through unification and critical pair computation. Frank report 41, Institut für Informatik. Fachbereich Informatik und Mathematik. Goethe-Universität Frankfurt am Main, January 2011.
bib | PDF | previous version ]
[2011] Manfred Schmidt-Schauß, editor. Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, RTA 2011, May 30 - June 1, 2011, Novi Sad, Serbia, volume 10 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011.
bib ]
[2010] Conrad Rau and Manfred Schmidt-Schauß. Towards correctness of program transformations through unification and critical pair computation. In Proceedings of the 24th International Workshop on Unification, volume 42 of Electronic Proceedings in Theoretical Computer Science, pages 39-54, December 2010.
bib | PDF ]
[2010] Manfred Schmidt-Schauß and Georg Schnitger. Fast equality test for straight-line compressed strings. unpublished manuscript, October 2010.
bib | superseded by Frank-45 | PDF | previous version ]
[2010] Manfred Schmidt-Schauß and David Sabel. A termination proof of reduction in a simply typed calculus with constructors. Frank report 42, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, October 2010.
bib | PDF ]
[2010] Manfred Schmidt-Schauß, David Sabel, and Elena Machkasova. Simulation in the call-by-need lambda-calculus with letrec. In Christopher Lynch, editor, Proceedings of the 21st International Conference on Rewriting Techniques and Applications, volume 6 of Leibniz International Proceedings in Informatics (LIPIcs), pages 295-310, Dagstuhl, Germany, July 2010. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.
bib | DOI | PDF | http ]
[2010] Manfred Schmidt-Schauß, David Sabel, and Elena Machkasova. Simulation in the call-by-need lambda-calculus with letrec. Frank report 40, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, April 2010.
bib | PDF ]
[2010] Adrià Gascón, Guillem Godoy, Manfred Schmidt-Schauß, and Ashish Tiwari. Context unification with one context variable. J. Symb. Comput., 45(2):173-193, 2010.
bib | DOI ]
[2010] Matthias Mann and Manfred Schmidt-Schauß. Similarity implies equivalence in a class of non-deterministic call-by-need lambda calculi. Information and Computation, 208(3):276 - 291, 2010.
bib | DOI | http ]
[2010] Manfred Schmidt-Schauß and David Sabel. On generic context lemmas for higher-order calculi with sharing. Theoretical Computer Science, 411(11-13):1521 - 1541, 2010.
bib | DOI | http ]
[2010] Manfred Schmidt-Schauß and David Sabel. Closures of may-, should- and must-convergences for contextual equivalence. Information Processing Letters, 110(6):232 - 235, 2010.
bib | DOI | http ]
[2009] David Sabel, Manfred Schmidt-Schauß, and Frederik Harwath. Reasoning about contextual equivalence: From untyped to polymorphically typed calculi. In Stefan Fischer, Erik Maehle, and Rüdiger Reischuk, editors, INFORMATIK 2009, Im Focus das Leben, Beiträge der 39. Jahrestagung der Gesellschaft für Informatik e.V. (GI), 28.9 - 2.10.2009 in Lübeck, volume 154 of GI Edition - Lecture Notes in Informatics, pages 369; 2931-45, October 2009. (4. Arbeitstagung Programmiersprachen (ATPS)), © Gesellschaft f�r Informatik e.V.
bib | PDF | previous version ]
[2009] Manfred Schmidt-Schauß, Elena Machkasova, and David Sabel. Counterexamples to simulation in non-deterministic call-by-need lambda-calculi with letrec. Frank report 38, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, August 2009.
bib | PDF ]
[2009] Jan Schwinghammer, David Sabel, Manfred Schmidt-Schauß, and Joachim Niehren. Correctly translating concurrency primitives. In ML '09: Proceedings of the 2009 ACM SIGPLAN workshop on ML, pages 27-38, New York, NY, USA, August 2009. ACM. ©ACM.
bib | PDF | http ]
[2009] Adrià Gascón, Guillem Godoy, and Manfred Schmidt-Schauß. Unification with singleton tree grammars. In 20. RTA 2009, volume 5595 of LNCS, pages 365-379. Springer, June 2009. ©Springer Verlag.
bib | PDF ]
[2009] Jan Schwinghammer, David Sabel, Joachim Niehren, and Manfred Schmidt-Schauß. On correctness of buffer implementations in a concurrent lambda calculus with futures. Frank report 37, Institut für Informatik. Fachbereich Informatik und Mathematik. Goethe-Universität Frankfurt am Main, May 2009.
bib | PDF | previous version ]
[2009] Markus Lohrey, Sebastian Maneth, and Manfred Schmidt-Schauß. Parameter reduction in grammar-compressed trees. In 12th FoSSaCS, volume 5504 of LNCS, pages 212-226. Springer, March 2009. ©Springer Verlag.
bib | PDF ]
[2009] Manfred Schmidt-Schauß, Joachim Niehren, Jan Schwinghammer, and David Sabel. Adequacy of compositional translations for observational semantics. Frank report 33, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, February 2009.
bib | PDF | previous version (4.0) | previous version (3.0) | previous version (2.0) | previous version (1.0) ]
[2009] Manfred Schmidt-Schauß, David Sabel, and Frederik Harwath. Contextual equivalence in lambda-calculi extended with letrec and with a parametric polymorphic type system. Frank report 36, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, January 2009.
bib | PDF ]
[2008] Manfred Schmidt-Schauß and David Sabel. Closures of may and must convergence for contextual equivalence. Frank report 35, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, December 2008.
bib | PDF ]
[2008] Jan Schwinghammer, David Sabel, Joachim Niehren, and Manfred Schmidt-Schauß. On proving the equivalence of concurrency primitives. Frank report 34, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, October 2008.
bib | PDF ]
[2008] Manfred Schmidt-Schauß and Matthias Mann. On equivalences and standardization in a non-deterministic call-by-need lambda calculus. Frank report 31, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, September 2008.
bib | PDF | previous version (2.0) | previous version (1.0) ]
[2008] Manfred Schmidt-Schauß, Joachim Niehren, Jan Schwinghammer, and David Sabel. Adequacy of compositional translations for observational semantics. In Giorgio Ausiello, Juhani Karhumäki, Giancarlo Mauri, and C.-H. Luke Ong, editors, Fifth IFIP International Conference On Theoretical Computer Science - TCS 2008, IFIP 20th World Computer Congress, TC 1, Foundations of Computer Science, September 7-10, 2008, Milano, Italy, volume 273 of IFIP, pages 521-535. Springer, September 2008. ©Springer Verlag.
bib ]
[2008] Manfred Schmidt-Schauß and Elena Machkasova. A finite simulation method in a non-deterministic call-by-need lambda-calculus with letrec, constructors and case. In Rewriting Techniques and Applications (RTA-18), volume 5117 of LNCS, pages 321-335. Springer-Verlag, July 2008. ©Springer Verlag.
bib | PDF | http ]
[2008] Adrià Gascón, Guillem Godoy, and Manfred Schmidt-Schauß. Context matching for compressed terms. In 23rd Annual IEEE Symposium on Logic in Computer Science (LICS 2008), pages 93-102. IEEE Computer Society, June 2008.
bib | http ]
[2008] Manfred Schmidt-Schauß and Elena Machkasova. A finite simulation method in a non-deterministic call-by-need calculus with letrec, constructors and case. Frank report 32, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, February 2008.
bib | PDF | previous version (1.0) ]
[2008] Jordi Levy, Manfred Schmidt-Schauß, and Mateu Villaret. The complexity of monadic second-order unification. SIAM J. of Computing, 38(3):1113-1140, 2008. the original publication is available at: http://epubs.siam.org/SICOMP/sicomp_toc.html, ©Siam J. of Computing 2008.
bib | PDF | http ]
[2008] David Sabel and Manfred Schmidt-Schauß. A call-by-need lambda-calculus with locally bottom-avoiding choice: Context lemma and correctness of transformations. Math. Structures Comput. Sci., 18(03):501-553, 2008.
bib | http ]
[2008] Manfred Schmidt-Schauß, Marko Schütz, and David Sabel. Safety of Nöcker's strictness analysis. J. Funct. Programming, 18(04):503-551, 2008. The original publication is available here, ©Cambridge University Press.
bib | DOI | appendix | PDF | http ]
[2007] Manfred Schmidt-Schauß and David Sabel. On generic context lemmas for lambda calculi with sharing. Frank report 27, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, August 2007.
bib | PDF | previous version (2.0) | previous version (1.0) ]
[2007] Manfred Schmidt-Schauß, David Sabel, and Marko Schütz. Deciding inclusion of set constants over infinite non-strict data structures. RAIRO-Theoretical Informatics and Applications, 41(2):225-241, July 2007. The original publication is available at: www.edpsciences.org/ita, © EDP Sciences 2007.
bib | PDF | http ]
[2007] Manfred Schmidt-Schauß. Correctness of copy in calculi with letrec. In Term Rewriting and Applications (RTA-18), volume 4533 of LNCS, pages 329-343. Springer, June 2007. ©Springer Verlag.
bib | slides (RTA 2007) ]
[2007] Joachim Niehren, David Sabel, Manfred Schmidt-Schauß, and Jan Schwinghammer. Observational semantics for a concurrent lambda calculus with reference cells and futures. Electronic Notes in Theoretical Computer Science, 173:313-337, April 2007. ©Elsevier B.V.
bib | DOI | http ]
[2007] Manfred Schmidt-Schauß and David Sabel. Program transformation for functional circuit descriptions. Frank report 30, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, February 2007.
bib | PDF ]
[2007] Manfred Schmidt-Schauß. Correctness of copy in calculi with letrec, case, constructors and por. Frank report 29, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, February 2007.
bib | PDF ]
[2007] M. Schmidt-Schauß. Correctness of copy in calculi with letrec, case and constructors. Frank report 28, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, February 2007.
bib | PDF ]
[2006] Joachim Niehren, David Sabel, Manfred Schmidt-Schauß, and Jan Schwinghammer. Program equivalence for a concurrent lambda calculus with futures. Frank report 26, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, October 2006.
bib | PDF ]
[2006] Manfred Schmidt-Schauß. Equivalence of call-by-name and call-by-need for lambda-calculi with letrec. Frank report 25, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, September 2006.
bib | PDF | previous version ]
[2006] Jordi Levy, Manfred Schmidt-Schauß, and Mateu Villaret. Stratified context unification is NP-complete. In Automated Reasoning (3rd IJCAR 2006), volume 4130 of LNCS, pages 82-96. Springer, August 2006. ©Springer Verlag.
bib ]
[2006] Jordi Levy, Manfred Schmidt-Schauß, and Mateu Villaret. Bounded second-order unification is NP-complete. In Term Rewriting and Applications (RTA-17), volume 4098 of LNCS, pages 400-414. Springer, August 2006. ©Springer Verlag.
bib ]
[2006] David Sabel and Manfred Schmidt-Schauß. A call-by-need lambda-calculus with locally bottom-avoiding choice: Context lemma and correctness of transformations. Frank report 24, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, July 2006.
bib | PDF | previous version ]
[2006] Manfred Schmidt-Schauß, David Sabel, and Marko Schütz. Deciding subset relationship of co-inductively defined set constants. Frank report 23, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, 2006.
bib | PDF | previous version ]
[2006] Matthias Mann and Manfred Schmidt-Schauß. How to prove similarity a precongruence in non-deterministic call-by-need lambda calculi. Frank report 22, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, January 2006.
bib | PDF ]
[2005] Manfred Schmidt-Schauß. Polynomial equality testing for terms with shared substructures. Frank report 21, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, November 2005.
bib | PDF ]
[2005] Manfred Schmidt-Schauß, Marko Schütz, and David Sabel. A complete proof of the safety of Nöcker's strictness analysis. Frank report 20, Institut für Informatik. J.W.Goethe-Universität Frankfurt am Main, April 2005.
bib | PDF ]
[2005] Manfred Schmidt-Schauß and Klaus U. Schulz. Decidability of bounded higher-order unification. J. Symbolic Computation, 40(2):905-954, 2005. © Elsevier B.V.
bib ]
[2005] Manfred Schmidt-Schauß. Decidable variants of higher-order unification. In Dieter Hutter and Werner Stephan, editors, Mechanizing Mathematical Reasoning, volume 2605 of Lecture Notes in Computer Science, pages 154-168. Springer, 2005.
bib ]
[2004] Manfred Schmidt-Schauß, Marko Schütz, and David Sabel. On the safety of Nöcker's strictness analysis. Frank Report 19, Institut für Informatik, J.W. Goethe-Universität Frankfurt am Main, October 2004.
bib | PDF ]
[2004] Manfred Schmidt-Schauß. Decidability of bounded second order unification. Information and Computation, 188(2):143-178, 2004. ©Elsevier B.V.
bib ]
[2004] Jordi Levy, Manfred Schmidt-Schauß, and Matteu Villaret. Monadic second-order unification is NP-complete. In Rewriting Techniques and Applications (RTA-15), LNCS 3091, pages 55-69. Springer, 2004. ©Springer Verlag.
bib ]
[2004] Manfred Schmidt-Schauß and Jürgen Stuber. On the complexity of linear and stratified context matching problems. Theory of Computing Systems, 37:717-740, 2004. © Springer Verlag.
bib ]
[2003] Manfred Schmidt-Schauß. FUNDIO: A Lambda-Calculus with a letrec, case, Constructors, and an IO-Interface: Approaching a Theory of unsafePerformIO. Frank report 16, Institut für Informatik, J.W. Goethe-Universität Frankfurt am Main, September 2003.
bib | compressed PostScript | PostScript | PDF ]
[2003] Manfred Schmidt-Schauß. Decidability of arity-bounded higher-order matching. In CADE-19, LNCS 2741, pages 488-502. Springer, 2003. ©Springer Verlag.
bib ]
[2002] Manfred Schmidt-Schauß and Klaus U. Schulz. Solvability of context equations with two context variables is decidable. Journal of Symbolic Computation, 33(1):77-122, 2002. © Elsevier B.V.
bib ]
[2002] Manfred Schmidt-Schauß and Klaus U. Schulz. Decidability of bounded higher-order unification. In CSL 2002, LNCS 2471, pages 522-536. Springer-Verlag, 2002. ©Springer Verlag.
bib ]
[2002] Manfred Schmidt-Schauß. A decision algorithm for stratified context unification. Journal of Logic and Computation, 12(6):929-953, 2002. ©Journal of Logic and Computation.
bib ]
[2001] Pok-Son Kim and Manfred Schmidt-Schauß. A term-based approach to project scheduling. In International Conference on Conceptual Structures, LNCS 2120, pages 304-318. Springer-Verlag, 2001. ©Springer Verlag.
bib ]
[2001] Manfred Schmidt-Schauß. Stratified context unification is in PSPACE. In CSL 2001, LNCS 2142, pages 498-512. Springer-Verlag, 2001. ©Springer Verlag.
bib ]
[2001] Manfred Schmidt-Schauß and Jürgen Stuber. On the complexity of linear and stratified context matching problems. Frank report 14, Institut für Informatik,J.W. Goethe-Universität Frankfurt am Main, 2001.
bib | compressed PostScript | PostScript ]
[2001] Manfred Schmidt-Schauß and Klaus U. Schulz. Decidability of bounded higher order unification. Frank report 15, Institut für Informatik, J.W. Goethe-Universität Frankfurt am Main, 2001.
bib | compressed PostScript | PostScript ]
[2000] Manfred Schmidt-Schauß. An Optimised Decision Algorithm for Stratified Context Unification. Frank report 13, Fachbereich Informatik, J.W. Goethe-Universität Frankfurt am Main, 2000.
bib | compressed PostScript | PostScript ]
[2000] Manfred Schmidt-Schauß and Michael Huber. A lambda-calculus with letrec, case, constructors and non-determinism. In First International Workshop on Rule-Based Programming, 2000.
bib ]
[1999] Manfred Schmidt-Schauß and Klaus U. Schulz. Solvability of context equations with two context variables is decidable. In International Conference on Automated Deduction, number 1632 in Lecture Notes in Computer Science, pages 67-81. Springer-Verlag, 1999. ©Springer Verlag.
bib ]
[1999] Manfred Schmidt-Schauß. Decidability of Bounded Second Order Unification. Frank report 11, Fachbereich Informatik, J.W. Goethe-Universität Frankfurt am Main, 1999.
bib | compressed PostScript | PostScript ]
[1999] Manfred Schmidt-Schauß. Decidability of behavioural equivalence in unary PCF. Theoretical Computer Science, 216:363-373, 1999. © Elsevier B.V.
bib | PostScript ]
[1999] Manfred Schmidt-Schauß and Marko Schütz (eds.). 13th international workshop on unification. Technical report, FB Informatik, J.W. Goethe-Universität Frankfurt am Main, 1999. internal report 6/99.
bib ]
[1999] Manfred Schmidt-Schauß. A Decision Algorithm for Stratified Context Unification. Frank report 12, Fachbereich Informatik, J.W. Goethe-Universität Frankfurt am Main, 1999.
bib | compressed PostScript | PostScript ]
[1998] Manfred Schmidt-Schauß and Klaus U. Schulz. On the exponent of periodicity of minimal solutions of context equations. In Proc. Rewriting Techniques and Applications, number 1379 in Lecture Notes in Computer Science, pages 61-75. Springer-Verlag, 1998. ©Springer Verlag.
bib | PostScript ]
[1998] Manfred Schmidt-Schauß. A decision algorithm for distributive unification. Theoretical Computer Science, 208:111-148, 1998. © Elsevier B.V.
bib | PostScript ]
[1998] Arne Kutzner and Manfred Schmidt-Schauß. A nondeterministic call-by-need lambda calculus. In International Conference on Functional Programming 1998, pages 324-335. ACM Press, 1998.
bib | compressed PostScript | PostScript | PDF ]
[1998] Manfred Schmidt-Schauß and Klaus U. Schulz. Solvability of context equations with two variables is decidable. Technical Report CIS-Report 98-114, Centrum für Informations- und Sprachverarbeitung (CIS), Universität München, 1998.
bib ]
[1997] M. Schütz and M. Schmidt-Schauß. Automatic Extraction of Context Information from Programs Using Abstract Reduction. Frank report 08, Fachbereich Informatik, J.W. Goethe-Universität Frankfurt am Main, May 1997.
bib | compressed PostScript | PostScript ]
[1997] Sven Eric Panitz and Manfred Schmidt-Schauß. Proving termination of higher-order functional programs with a tableau-like calculus. Technical report, CRIN-CNRS, 1997. Tableaux'97 position paper.
bib | PostScript ]
[1997] Nigel W. O. Hutchison, Ute Neuhaus, Manfred Schmidt-Schauß, and Cordelia V. Hall. Natural expert: A commercial functional programming environment. J. of Functional Programming, 7(2):163-182, 1997.
bib ]
[1997] Sven Eric Panitz and Manfred Schmidt-Schauß. TEA: automatically proving termination of programs in non-strict higher-order functional language. In Static Analysis, 4th international symposium, number 1302 in Lecture Notes in Computer Science, pages 345-360. Springer-Verlag, 1997. ©Springer Verlag.
bib | PostScript ]
[1996] Manfred Schmidt-Schauß. A Partial Rehabilitation of Side-Effecting I/O: Non-Determinism in Non-Strict Functional Languages. Frank report 07, Fachbereich Informatik, J.W. Goethe-Universität Frankfurt am Main, June 1996.
bib | compressed PostScript | PostScript ]
[1996] Manfred Schmidt-Schauß. An algorithm for distributive unification. In Proc. of the Conf. on Rewriting Techniques and Applications, number 1103 in Lecture Notes in Computer Science, pages 287-301. Springer-Verlag, 1996. ©Springer Verlag.
bib | compressed PostScript | PostScript ]
[1996] Manfred Schmidt-Schauß. CPE: A Calculus for Proving Equivalence of Expressions in a Non-Strict Functional Language. Frank report (internal report 2/96) 05, Fachbereich Informatik, J.W. Goethe-Universität Frankfurt am Main, 1996.
bib | compressed PostScript | PostScript ]
[1996] Manfred Schmidt-Schauß. Decidability of unification in the theory of one-sided distributivity and a multiplicative unit. J. Symbolic Computation, 22(3):315-344, 1996. © Elsevier B.V.
bib | PostScript | PDF ]
Unification in the equational theory of one-sided distributivity and a multiplicative unit is shown to be decidable. The algorithm is a non-deterministic one that eventually uses a decision algorithm for string unification problems with constant restrictions, which was shown to be decidable by K. Schulz extending the decision algorithm for string unification by Makanin.

[1995] Manfred Schmidt-Schauß, Massimo Marchiori, and Sven Eric Panitz. Modular Termination of r-Consistent and Left-Linear Term Rewriting Systems. Theoretical Computer Science, 150(1):361-374, 1995. © Elsevier B.V.
bib | compressed PostScript | PostScript | PDF ]
[1995] Manfred Schmidt-Schauß. On the Semantics and Interpretation of Rule Based Programs with Static Global Variables. Frank report (internal report 8/95) 04, Fachbereich Informatik, J.W. Goethe-Universität Frankfurt am Main, 1995.
bib | compressed PostScript | PostScript ]
[1995] Manfred Schmidt-Schauß, Sven Eric Panitz, and Marko Schütz. Strictness analysis by abstract reduction using a tableau calculus. In Proc. of the Static Analysis Symposium, number 983 in Lecture Notes in Computer Science, pages 348-365. Springer-Verlag, 1995. ©Springer Verlag.
bib | compressed PostScript | PostScript ]
[1995] M. Schütz, M. Schmidt-Schauß, and S.E. Panitz. Efficient Strictness Analysis of Haskell in Haskell Using Abstract Reduction. Frank report 09, Fachbereich Informatik,J.W. Goethe-Universität Frankfurt am Main, 1995.
bib | compressed PostScript | PostScript ]
[1994] Manfred Schmidt-Schauß. Unification of stratified second-order terms. Technical Report 12/94, FB Informatik, J.W. Goethe-Universität Frankfurt am Main, 1994.
bib | compressed PostScript | PostScript ]
[1994] Manfred Schmidt-Schauß. An Algorithm for Distributive Unification. Frank report (internal report 13/94) 02, Fachbereich Informatik, J.W. Goethe-Universität Frankfurt am Main, 1994.
bib | compressed PostScript | PostScript ]
[1994] B. Pohl, C. Beringer, S. Walther, J. Melzer, F. Burow, M. Schmidt-Schauß, and Chr. Trendelenburg. Neue Befundungsverfahren zur Erstellung wissensbasierter Befundungssysteme mit der Expertensystemschale Pro.M.D. Laboratoriumsmedizin, 18(12):577-582, 1994. in German.
bib ]
[1993] Manfred Schmidt-Schauß. Unification under one-sided distributivity with a multiplicative unit. In Proc. LPAR '93, number 698 in Lecture Notes in Computer Science, pages 289-300. Springer-Verlag, 1993. ©Springer Verlag.
bib ]
[1992] Manfred Schmidt-Schauß. Some results on unification in distributive equational theories. Technical Report 7/92, FB Informatik, J.W. Goethe-Universität Frankfurt am Main, 1992.
bib ]
[1991] Manfred Schmidt-Schauß and Gert Smolka. Attributive concept descriptions with complements,. Artificial Intelligence, 48:1-26, 1991.
bib ]
[1991] Manfred Schmidt-Schauß. External function calls in a functional language. In Proc. of the 1991 Glasgow Workshop on Functional Programming, Workshops in Computing, pages 324-331. Springer-Verlag, 1991.
bib ]
[1990] Bernhard Hollunder, Werner Nutt, and Manfred Schmidt-Schauß. Subsumption algorithms for concept description languages. In Proc. of 9th European Conference on Artificial Intelligence, 1990.
bib ]
[1989] Alexandre Boudet, Jean-Pierre Jouannaud, and Manfred Schmidt-Schauß. Unification in boolean rings and abelian groups. J. Symbolic Computation, 8:449-477, 1989. © Elsevier B.V.
bib ]
[1989] Manfred Schmidt-Schauß. Unification in permutative theories is undecidable. J. Symbolic Computation, 8:415-421, 1989. © Elsevier B.V.
bib | PDF ]
[1989] Hans-Jürgen Bürckert, Alexander Herold, and Manfred Schmidt-Schauß. On equational theories, unification and (un)decidability. J. Symbolic Computation, 8:3-49, 1989. © Elsevier B.V.
bib ]
[1989] Manfred Schmidt-Schauß. Unification in a combination of arbitrary disjoint equational theories. J. Symbolic Computation, 8:51-99, 1989. © Elsevier B.V.
bib ]
[1989] Manfred Schmidt-Schauß. Computational Aspects of an Order-sorted Logic with Term Declarations. Number 395 in Lecture Notes in Computer Science. Springer-Verlag, 1989. ©Springer Verlag.
bib ]
[1989] Hans-Jürgen Bürckert and Manfred Schmidt-Schauß. Some solvability results for equational problems. Technical Report SEKI-report SR-89-07, FB Informatik, Universität Kaiserslautern, 1989.
bib ]
[1989] Manfred Schmidt-Schauß. Subsumption in KL-ONE is undecidable. In Proc. of 1st Conf. on Knowledge Representation and Reasoning, pages 421-431, 1989.
bib | PostScript | PDF ]
[1988] Manfred Schmidt-Schauß. Implication of clauses is undecidable,. Theoretical Computer Science, 59(3):287-296, 1988. © Elsevier B.V.
bib ]
[1988] Manfred Schmidt-Schauß. Unification in a combination of arbitrary disjoint equational theories,. In Proc. of 9th Conference on Automated Deduction, volume 310 of Lecture Notes in Computer Science, pages 378-396. Springer-Verlag, 1988. ©Springer Verlag.
bib ]
[1988] Manfred Schmidt-Schauß. Computational Aspects of an Order-sorted Logic with Term Declarations. PhD thesis, FB Informatik, Universität Kaiserslautern, 1988. (SEKI-report SR-88-10).
bib ]
[1988] Alexandre Boudet, Jean-Pierre Jouannaud, and Manfred Schmidt-Schauß. Unification in boolean rings and abelian groups. In Third Symp. on Logic in Computer Science, 1988.
bib ]
[1988] Manfred Schmidt-Schauß and Jörg Siekmann. Unification algebras: An axiomatic approach to unification, equation solving and constraint solving. Technical Report SEKI-report SR-88-09, FB Informatik, Universität Kaiserslautern, 1988.
bib | PDF ]
[1988] Manfred Schmidt-Schauß. Subsumption in KL-ONE is undecidable. Technical Report SEKI-report SR-88-13, FB Informatik, Universität Kaiserslautern, 1988.
bib ]
[1988] Manfred Schmidt-Schauß and Gert Smolka. Attributive concept descriptions with complements. Technical Report SEKI-report SR-88-21, FB Informatik, Universität Kaiserslautern, 1988. also: IWBS-report 68, IBM Deutschland, Juni 1989).
bib ]
[1987] Hans-Jürgen Bürckert, Alexander Herold, and Manfred Schmidt-Schauß. On equational theories, unification and decidability. In Rewriting Techniques and Application, volume 256 of Lecture Notes in Computer Science, pages 204-215. Springer-Verlag, 1987. ©Springer Verlag.
bib ]
[1987] Manfred Schmidt-Schauß. Unification in permutative equational theories is undecidable. Technical Report SEKI-report SR-87-03, FB Informatik, Universität Kaiserslautern, 1987.
bib ]
[1987] Manfred Schmidt-Schauß. Unification in a combination of arbitrary disjoint equational theories. Technical Report SEKI-report SR-87-16, FB Informatik, Universität Kaiserslautern, 1987.
bib ]
[1986] Manfred Schmidt-Schauß. Unification in many-sorted equational theories. In Proc. of 8th Conference on Automated Deduction, volume 230 of Lecture Notes in Computer Science, pages 538-552. Springer-Verlag, 1986. ©Springer Verlag.
bib ]
[1986] Manfred Schmidt-Schauß. Unification under associativity and idempotence is of type nullary. J. Automated Reasoning, 2(3):227-281, 1986.
bib ]
[1986] Manfred Schmidt-Schauß. Unification properties of idempotent semigroups. Technical Report SEKI-report SR-86-07, FB Informatik, Universität Kaiserslautern, 1986.
bib ]
[1986] Manfred Schmidt-Schauß. Some undecidable classes of clause sets. Technical Report SEKI-report SR-86-08, FB Informatik, Universität Kaiserslautern, 1986.
bib ]
[1986] Hans-Jürgen Bürckert, Alexander Herold, and Manfred Schmidt-Schauß. On equational theories, unification and decidability. Technical Report SEKI-report SR-86-20, FB Informatik, Universität Kaiserslautern, 1986.
bib ]
[1985] Manfred Schmidt-Schauß. A many-sorted calculus with polymorphic functions based on resolution and paramodulation. In Proc. of 9th International Joint Conference on Artificial Intelligence, pages 1162-1168, 1985.
bib ]
[1985] Manfred Schmidt-Schauß. A many-sorted calculus with polymorphic functions based on resolution and paramodulation. Technical Report SEKI-report MK-85-2, FB Informatik, Universität Kaiserslautern, 1985.
bib ]
[1985] Manfred Schmidt-Schauß. Mechanical generation of sorts in clause sets. Technical Report SEKI-report MK-85-6, FB Informatik, Universität Kaiserslautern, 1985.
bib ]
[1985] Manfred Schmidt-Schauß. Unification in a many-sorted calculus with declarations. In H. Stoyan, editor, Proc. of 9th German Workshop on Artificial Intelligence, volume 118 of Informatik Fachberichte, pages 118-132. Springer-Verlag, 1985.
bib ]
[1985] Hans Jürgen Ohlbach and Manfred Schmidt-Schauß. The lion and the unicorn. J. Automated Reasoning, 1:327-332, 1985.
bib ]

This file was generated by bibtex2html 1.97.


$Author: dallmeyer $, $Date: 2018/06/14 13:39:13 $

uni ffm © 1997, 2004