MPI-INF Logo

Publications

Search the publication database
.
Return

Your search returned the following 54 documents:

  1. Logical Frameworks
    David A. Basin and Sean Matthews
    In: Handbook of Philosophical Logic, 2002, 89-164
  2. A Higher-order Interpretation of Deductive Tableau
    Abdelwaheb Ayari and David A. Basin
    Journal of Symbolic Computation 31 (5): 487-520, 2001
  3. Automated Complexity Analysis Based on Ordered Resolution
    David A. Basin and Harald Ganzinger
    Journal of the ACM 48 (1): 70-109, 2001
    [PS: Download: 2001JACM.ps.gz]
  4. Program Development Schemata as Derived Rules
    Penny Anderson and David A. Basin
    Journal of Symbolic Computation 30 (1): 5-36, 2000
  5. Structuring Metatheory on Inductive Definitions
    Seán Matthews and David A. Basin
    Information and Computation 162 (1/2): 80-95, 2000
  6. Formalization of the Development Process
    David A. Basin and Bernd Krieg-Brückner
    In: Algebraic foundations of systems specification, 1999, 521-562
  7. Modeling a Hardware Synthesis Methodology in Isabelle
    David A. Basin and Stefan Friedrich
    Formal Methods in Systems Design 15 (2): 99-122, 1999
  8. A Modular Presentation of Modal Logics in a Logical Framework
    David A. Basin, Seán Matthews, and Luca Viganò
    In: Proceedings of the 1st Tbilisi Symposium on Language, Logic and Computation: Selected Papers, Tbilisi, Georgia, October 1995, 1998, 293-307
  9. Automata Based Symbolic Reasoning in Hardware Verification
    David A. Basin and Nils Klarlund
    Formal Methods in Systems Design 13 (3): 255-288, 1998
  10. Labelled Modal Logics: quantifiers
    David A. Basin, Seán Matthews, and Luca Viganò
    Journal of Logic, Language and Information 7 (3): 237-263, 1998
  11. LISA: A Specification Language Based on WS2S
    Ayari Abdelwaheb, David A. Basin, and Andreas Podelski
    In: Proceedings of the 11th International Workshop on Computer Science Logic (CSL-97), Aarhus, Denmark, August, 23 - 29, 1998, 18-34
  12. Natural Deduction for Non-Classical Logics
    David A. Basin, Seán Matthews, and Luca Viganò
    Studia Logica 60 (1): 119-160, 1998
  13. Scoped Metatheorems
    Seán Matthews and David A. Basin
    Electronic Notes in Computer Science 15: 1-14, 1998
  14. Search in Games with Incomplete Information: A Case Study Using Bridge Card Play
    Ian Frank and David A. Basin
    Artificial Intelligence 100 (1/2): 87-123, 1998. Note: Also available as Research Paper
  15. A New Method for Bounding the Complexity of Modal Logics
    David A. Basin, Seán Matthews, and Luca Viganò
    In: Proceedings of the 5th Kurt Gödel Colloquium on Computational Logic and Proof Theory (KGC-97), Vienna, Austria, August, 25 - 29, 1997, 89-102
  16. Labelled Propositional Modal Logics: Theory and Practice
    David A. Basin, Seán Matthews, and Luca Viganò
    Journal of Logic and Computation 7 (6): 685-717, 1997
  17. Labelled quantified modal logics
    David A. Basin, Seán Matthews, and Luca Viganò
    In: Proceedings of the 21st Annual German Conference on Artificial Intelligence (KI-97): Advances in Artificial Intelligence, Freiburg, Germany, September, 1997, 171-182
  18. A Calculus for and Termination of Rippling
    David A. Basin and Toby Walsh
    Journal of Automated Reasoning 16 (1/2): 147-180, 1996
  19. A Calculus for and Termination of Rippling
    David A. Basin and Toby Walsh
    In: Automated mathematical induction, 1996, 147-180. Note: Reprinted from Journal of Automated Reasoning 16 (Nos. 1/2)
  20. A Topography of Labelled Modal Logics
    David A. Basin, Seán Matthews, and Luca Viganò
    In: Frontiers of Combining Systems (First International Workshop, Munich, March 1996), 1996, 75-92
  21. Adding Metatheoretic facilities to First-order Theories
    David A. Basin and Seán Matthews
    Journal of Logic and Computation 6 (6): 835-849, 1996
  22. Complexity Analysis Based on Ordered Resolution
    David A. Basin and Harald Ganzinger
    In: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (LICS'96), New Brunswick, New Jersey, USA, July 27-30, 1996, 1996, 456-465
  23. Experiments in Automating Hardware Verification using Inductive Proof Planning
    Francisco Cantu, Alan Bundy, Alan Smaill, and David A. Basin
    In: Proceedings of the Formal Methods for Computer-Aided Design Conference (FMCAD'96), Palo Alto, CA, USA, 1996, 94-108
  24. Generic System Support for Deductive Program Development
    Abdelwaheb Ayari and David A. Basin
    In: Second International Workshop, TACAS'96: Tools and Algorithms for the Construction and Analysis of Systems, Passau, Germany, March, 1996, 313-328
  25. Implementing Modal and Relevance Logics in a Logical Framework
    David A. Basin, Seán Matthews, and Luca Viganò
    In: Proceedings of the 5th International Conference on Principles of Knowledge Representation and Reasoning (KR'96), Cambridge, MA, USA, November 5-8, 1996, 1996, 386-397
  26. Middle-out reasoning for synthesis and induction
    Ina Kraan, David A. Basin, and Alan Bundy
    Journal of Automated Reasoning 16 (1/2): 113-145, 1996
  27. Middle-Out Reasoning for Synthesis and Induction
    Ina Kraan, David A. Basin, and Alan Bundy
    In: Automated mathematical induction, 1996, 113-145. Note: Reprinted from Journal of Automated Reasoning 16 (Nos. 1/2)
  28. Modeling a hardware synthesis methodology in Isabelle
    David A. Basin and Stefan Friedrich
    In: Theorem Proving in Higher Order Logics. 9th International Conference, TPHOLs'96, Turku, Finland, August, 26-30, 1996, 33-50
  29. Search in Games with Incomplete Information: A Case Study Using Bridge Card Play
    Ian Frank and David A. Basin
    Department of Artificial Intelligence, Edinburgh, 780, Research Paper. Note: Also Available as journal article (Artificial Intelligence)
  30. Structuring metatheory on inductive definitions
    David A. Basin and Seán Matthews
    In: Proceedings of the 13th International Conference on Automated Deduction (CADE-13), New Brunswick, New Jersey, USA, July, 30 - August, 3, 1996, 171-185
  31. Deriving and Applying Logic Program Transformers
    Penny Anderson and David A. Basin
    In: Algorithms, Concurrency and Knowledge (1995 Asian Computing Science Conference), Pathumthani, Thailand, 1995, 1995, 301-318
  32. Hardware Verification using Monadic Second-Order Logic
    David A. Basin and Nils Klarlund
    In: Proceedings of the 7th International Conference on Computer-Aided Verification (CAV '95), Liege, Belgium, 1995, 1995, 31-41
  33. Interpretation of the Deductive Tableau in HOL
    Abdelwaheb Ayari and David A. Basin
    In: Proceedings of the First Isabelle Users Workshop, University of Cambridge, England, 18-19 September, 1995, 91-100
  34. Thema der Antrittsvorlesung: MONA - Ein Werkzeug zur Systemverifikation und -entwicklung
    David A. Basin
    Habilitation thesis, Universität des Saarlandes, 1995
  35. A Term Equality Problem Equivalent to Graph Isomorphism
    David A. Basin
    Information Processing Letters 51 (2): 61-66, 1994
  36. Coloured Rippling: An Extension of a Theorem Proving Heuristic
    Tetsuja Yoshida, Alan Bundy, Ian Green, Toby Walsh, and David A. Basin
    In: Proceedings of the 12th European Conference on Artificial Intelligence (ECAI'94), Amsterdam, Netherlands, 1994, 1994, 85-89
  37. Generalized Rewriting in Type Theory
    David A. Basin
    Journal of Information Processing and Cybernetics 30 (5/6): 249-259, 1994. Note: erschienen 1995 !!!
  38. Logic Frameworks for Logic Programs
    David A. Basin
    In: Proceedings of the 4th International Workshop on Logic Program Synthesis and Transformation - Meta Programming in Logic (LOPSTR'94 and META'94), Pisa, Italy, June, 20-21, 1994, 1994, 1-16. Note: Also available as Research Report MPI-I-94-218, Max-Planck-Institut für Informatik, Saarbrücken
  39. Termination Orderings for Rippling
    David A. Basin and Toby Walsh
    In: Proceedings of the 12th International Conference On Automated Deduction (CADE-12), Nancy, France, June 26 - July 1, 1994, 1994, 466-483. Note: Also available as Research Report MPI-I-94-209, Max-Planck-Institut für Informatik, Saarbrücken
  40. IsaWhelk: Whelk Interpreted in Isabelle
    David A. Basin
    In: Proceedings of the 11th International Conference on Logic Programming (ICLP'94), Santa Margherita Ligure, Italy, June 13-18, 1994, 1994, 741-741. Note: Paper is extended abstract. {F}ull version available via anonymous ftp to mpi-sb.mpg.de in pub/papers/conferences/Basin-ICLP94.dvi.Z
  41. A Conservative Extension of First-Order Logic and its Applications to Theorem Proving
    David A. Basin and Seán Matthews
    In: Proceedings of the 13th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'93), Bombay, India, 1993, 151-160. Note: Also available as Research Report MPI-I-93-235
  42. A Framework for Program Development Based on Schematic Proof
    David A. Basin, Alan Bundy, Ina Kraan, and Seán Matthews
    In: Proc. 7th Intern.~Workshop on Software Specification and Design, Redondo Beach, CA, 1993, 162-171. Note: Also available as Research Report MPI-I-93-231
  43. A Recursion Planning Analysis of Inductive Completion
    Richard Barnett, David A. Basin, and Jane Hesketh
    Annals of Mathematics and Artificial Intelligence 8 (3/4): 363-381, 1993. Note: Also available as Research Report MPI-I-92-230
  44. Difference Unification
    David A. Basin and Toby Walsh
    In: Proceedings of the 13th International Joint Conference on Artificial Intelligence (IJCAI-93), Chambery, France, 1993, 116-122. Note: Also available as Research Report MPI-I-92-247
  45. Experience with $FS_0$ as a Framework Theory
    Seán Matthews, Alan Smaill, and David A. Basin
    In: Logical Environments, 1993, 61-82. Note: Also available as Technical Report {MPI-I-92-214}
  46. Logic Program Synthesis via Proof Planning
    Ina Kraan, David A. Basin, and Alan Bundy
    In: International Workshop on Logic Program Synthesis and Transformation (LOPSTR '92), Manchester, UK, 1992, 1993, 1-14. Note: Also available as Research Report MPI-I-92-244
  47. Metalogical Frameworks
    David A. Basin and Robert L. Constable
    In: Logical Environments, 1993, 1-29. Note: Also available as Research Report MPI-I-92-205
  48. Middle-Out Reasoning for Logic Program Synthesis
    Ina Kraan, David A. Basin, and Alan Bundy
    In: Proc.~10th Intern. Conference on Logic Programing (ICLP '93), Budapest, Hungary, 1993, 441-455. Note: Also available as Research Report MPI-I-93-214
  49. Difference Matching
    David A. Basin and Toby Walsh
    In: Proceedings of the11th International Conference on Automated Deduction (CADE-11), Saragota Springs, NY, 1992, 295-309. Note: Also available as Research Report MPI-I-92-211
  50. Finesse: An Adaptation of Proof-Planning to Declarer Play in Bridge
    Ian Frank, David A. Basin, and Alan Bundy
    In: Proceedings of the 10th European Conference on Artificial Intelligence (ECAI-92), Vienna, Austria, 1992, 72-76
  51. Automating Meta-Theory Creation and System Extension
    David A. Basin, Fausto Giunchiglia, and P. Traverso
    In: Proc. Trends in AI: 2nd Congress of the Italian Association for Artificial Intelligence (AI*IA), Palermo, Italy, 1991, 48-57
  52. Formally Verified Synthesis of Combinational CMOS Circuits
    David A. Basin, G. M. Brown, and M. E. Leeser
    Integration: The Intern. Journal of VLSI Design 11: 235-250, 1991
  53. Some Normalization Properties of Martin-Löf's Type Theory, and Applications
    David A. Basin and D. Howe
    In: International Conference on Theoretical Aspects of Computer Software (TACS '91), Sendai, Japan, September 24-27, 1991, 475-494
  54. The Boyer-Moore Prover and Nuprl: An Experimental Comparison
    David A. Basin and Matt Kaufmann
    In: Logical Frameworks, 1991, 90-119