Your search returned the following 54 documents:
-
Logical Frameworks
David A. Basin and Sean Matthews
In: Handbook of Philosophical Logic, 2002, 89-164
-
A Higher-order Interpretation of Deductive Tableau
Abdelwaheb Ayari and David A. Basin
Journal of Symbolic Computation 31 (5): 487-520, 2001
-
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]
-
Program Development Schemata as Derived Rules
Penny Anderson and David A. Basin
Journal of Symbolic Computation 30 (1): 5-36, 2000
-
Structuring Metatheory on Inductive Definitions
Seán Matthews and David A. Basin
Information and Computation 162 (1/2): 80-95, 2000
-
Formalization of the Development Process
David A. Basin and Bernd Krieg-Brückner
In: Algebraic foundations of systems specification, 1999, 521-562
-
Modeling a Hardware Synthesis Methodology in Isabelle
David A. Basin and Stefan Friedrich
Formal Methods in Systems Design 15 (2): 99-122, 1999
-
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
-
Automata Based Symbolic Reasoning in Hardware Verification
David A. Basin and Nils Klarlund
Formal Methods in Systems Design 13 (3): 255-288, 1998
-
Labelled Modal Logics: quantifiers
David A. Basin, Seán Matthews, and Luca Viganò
Journal of Logic, Language and Information 7 (3): 237-263, 1998
-
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
-
Natural Deduction for Non-Classical Logics
David A. Basin, Seán Matthews, and Luca Viganò
Studia Logica 60 (1): 119-160, 1998
-
Scoped Metatheorems
Seán Matthews and David A. Basin
Electronic Notes in Computer Science 15: 1-14, 1998
-
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
-
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
-
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
-
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
-
A Calculus for and Termination of Rippling
David A. Basin and Toby Walsh
Journal of Automated Reasoning 16 (1/2): 147-180, 1996
-
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)
-
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
-
Adding Metatheoretic facilities to First-order Theories
David A. Basin and Seán Matthews
Journal of Logic and Computation 6 (6): 835-849, 1996
-
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
-
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
-
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
-
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
-
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
-
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)
-
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
-
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)
-
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
-
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
-
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
-
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
-
Thema der Antrittsvorlesung: MONA - Ein Werkzeug zur Systemverifikation und -entwicklung
David A. Basin
Habilitation thesis, Universität des Saarlandes, 1995
-
A Term Equality Problem Equivalent to Graph Isomorphism
David A. Basin
Information Processing Letters 51 (2): 61-66, 1994
-
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
-
Generalized Rewriting in Type Theory
David A. Basin
Journal of Information Processing and Cybernetics 30 (5/6): 249-259, 1994. Note: erschienen 1995 !!!
-
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
-
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
-
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
-
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
-
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
-
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
-
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
-
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}
-
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
-
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
-
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
-
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
-
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
-
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
-
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
-
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
-
The Boyer-Moore Prover and Nuprl: An Experimental Comparison
David A. Basin and Matt Kaufmann
In: Logical Frameworks, 1991, 90-119