The following is a list of ancient, recent or forthcoming reports and publications by Roy Dyckhoff and/or his students and collaborators at the St Andrews University School of Computer Science. For others in the Computational Logic Group, see their own web pages.
The links are mainly links to Postscript files. The files are usually not compressed. Sometimes there is a dvi file or a pdf file.
Accepted or published journal papers in final form are copyright of the publisher: RD may be able to send a preprint or offprint. Where a file is available directly via this page, it may be only a near-final version and the published version is normally the only one that should be cited.
R. Dyckhoff, Indefinite proof and inversions of syllogisms, Bulletin of Symbolic Logic, accepted 14 July 2018 Near-Final PDF
R. Dyckhoff, Contraction-free sequent calculi in intuitionistic logic: a correction, Journal of Symbolic Logic, accepted 18 May 2018, Near-Final PDF
R. Dyckhoff & S. Negri, Commentary on Grigori Mints' "Classical and Intuitionistic Geometric Logic", IfCoLog Journal of Logics and their Applications 4 (4), pp 1235--1239, 2017 URL
R. Dyckhoff, M. Sadrzadeh & J. Truffaut, Algebra, proof theory and applications for an intuitionistic logic of propositions, actions and adjoint modal operators, ACM Transactions on Computational Logic, published online, 2013. DOI: 10.1145/2536740.2536742. Abstract & PDF
R. Dyckhoff & S. Negri, A cut-free sequent system for Grzegorczyk logic, with an application to the Gödel-McKinsey-Tarski embedding, Journal of Logic and Computation, DOI: 10.1093/logcom/ext036. Abstract & PDF
S. Lengrand, R. Dyckhoff & J. McKinna, A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems, Logical Methods in Computer Science 7(1:6), pp. 1--35, 2011. DOI: 10.2168/LMCS-7(1:6)2011. Abstract, PDF
N. Francez & R. Dyckhoff, Proof-theoretic semantics for a natural language fragment, Linguistics & Philosophy 33, pp 447--477, 2010. Abstract, PDF
M. Sadrzadeh & R. Dyckhoff, Positive Logic with Adjoint Modalities: Proof Theory, Semantics and Reasoning about Information (full version), Review of Symbolic Logic 3: pp 351--373, 2010. Abstract, PDF
M. Sadrzadeh & R. Dyckhoff, Positive Logic with Adjoint Modalities: Proof Theory, Semantics and Reasoning about Information (short version), Electronic Notes in Theoretical Computer Science 249: pp 451--470, 2009. Abstract, PDF
R. Dyckhoff & S. Negri, Decision methods for linearly ordered Heyting algebras, Archive for Mathematical Logic 45(4), pp 411-422, 2006. Abstract. ISSN: 0933-5846 (print version), ISSN: 1432-0665 (electronic version)
R. Dyckhoff & C. Urban, Strong normalization of Herbelin's explicit substitution calculi with substitution propagation, Journal of Logic & Computation 13(5), pp 689--706, October 2003. Abstract, dvi, pdf, ps. (ISSN: 0955-792X)
R. Dyckhoff & S. Negri, Admissibility of structural rules for extensions of contraction-free sequent calculi, Logic Journal of the IGPL 9, pp 573--580, 2001, Abstract, dvi, pdf, ps. (Print ISSN: 1367-0751 Online ISSN: 1368-9894)
R. Dyckhoff & S. Negri, Admissibility of structural rules for contraction-free systems of intuitionistic logic, J. Symb. Logic 65, (December 2000), pp 1499--1518, Abstract, dvi, pdf, ps. (ISSN 0022-4812)
J. Caldwell, I. Gent & J. Underwood, Search Algorithms in Type Theory, Theoretical Computer Science 232, pp 55--90, 2000.
R. Dyckhoff, A Deterministic Terminating Sequent Calculus for Gödel-Dummett logic, Logic Journal of the IGPL 7, pp 319--326, 1999. Abstract, dvi, pdf, ps. (Print ISSN: 1367-0751 Online ISSN: 1368-9894)
L. Pinto & R. Dyckhoff, Sequent calculi for the normal terms of the Lambda-Pi and Lambda-Pi-Sigma calculi , June 1998, (Proceedings of the CADE15-Workshop on Proof Search in Type Theoretic Languages), Electronic Notes in Theoretical Computer Science 17, 1998, 13 pp, ps.
R. Dyckhoff & L. Pinto, Cut-elimination and a permutation-free sequent calculus for intuitionistic logic, Studia Logica 60, pp 107--118, 1998. pdf.
R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic, J. Symb. Logic 57, pp 795--807, 1992. (ISSN 0022-4812), pdf
R. Dyckhoff, Intuitionistic decision procedures since Gentzen, Advances in Proof Theory (eds. R Kahle, T Strahm, T Studer), Springer 18 pp, 2016.
R. Dyckhoff, Some remarks on proof-theoretic semantics, Proceedings of Second Tübingen Conference on Proof-Theoretic Semantics (March 2013) (ed. P Schroeder-Heister) in "Trends in Logic" 43, pp 79--93, Springer, 2015.
R. Dyckhoff, Cut-elimination, substitution and normalisation, Dag Prawitz on Proofs and Meaning (ed. H Wansing) in "Outstanding Contributions to Logic" 7, pp 163--189, Springer, 2015.
F. Ausaf, R. Dyckhoff, C. Urban, POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl) 17pp, ITP 2016, (Proceedings), Lecture Notes in Computer Science 9807, pp 69--86, Springer Verlag, PDF
R. Dyckhoff, S. Negri, Coherentisation of accessibility conditions in labelled sequent calculi, (Extended Abstract) "Gentzen Systems and Beyond" Workshop, Vienna Summer of Logic, 2pp, 13 July 2014, PDF
A. Kapsner, D. Miller, R. Dyckhoff, Report on Kalman Cohen's 1954 Oxford Thesis on Alternative Systems of Logic, New Directions in Paraconsistent Logic: 5th WCP, (Proceedings: ed J-Y Beziau et al), Kolkata, India, February 2014, p 61, Springer Verlag, PDF.
R. Dyckhoff, D. Kesner, S. Lengrand, Strong cut-elimination systems for Hudelmaier's depth-bounded sequent calculus for implicational logic, IJCAR 2006, (Proceedings, edited by U. Furbach and N. Shankar), Lecture Notes in Artificial Intelligence 4130, pp 347--361, Springer Verlag, PDF.
R. Dyckhoff, S. Lengrand, LJQ: a strongly focused calculus for intuitionistic logic, Computability in Europe 2006, (Proceedings, edited by A. Beckmann et al), LNCS vol 3988, pp 173--185, Springer Verlag, PDF.
K. Hammond, R. Dyckhoff, C. Ferdinand, R. Heckmann, M. Hofmann, S. Jost, H.-W. Loidl, G. Michaelson, R. Pointon, N. Scaife, J. érot, A. Wallace, Towards Formally Verifiable Resource Bounds for Real-Time Embedded Systems , Innovative Techniques for Certification of Embedded Systems, (Workshop Proceedings), PDF, 2006, 14pp.
K. Hammond, R. Dyckhoff, C. Ferdinand, R. Heckmann, M. Hofmann, S. Jost, H.-W. Loidl, G. Michaelson, R. Pointon, N. Scaife, J. Sérot, A. Wallace, Towards Formally Verifiable WCET Analysis for a Functional Programming Language, WCET 06, (Workshop Proceedings), PDF, 2006, pp 56--61.
K. Hammond, R. Dyckhoff, R. Heckmann, M. Hofmann, H.-W. Loidl, G. Michaelson, J. Sérot & A.Wallace, The EmBounded project (project paper), 6th Symposium on Trends in Functional Programming, TFP 2005, Tallinn, Estonia, September 23--24 2005, pdf.
R. Macinnis, J. McKinna, J. Parsons & R.Dyckhoff, A mechanised environment for Frege's Begriffsschrift notation, Workshop on Mathematical User Interfaces 2004, Bialowieza (Poland), September 18 2004, pdf.
R. Dyckhoff & C.Urban, Strong normalization of Herbelin's explicit substitution calculi with substitution propagation, (revised version), Proceedings of the Fourth Workshop on Explicit Substitutions: Theory and Applications (WESTAPP 01), Utrecht, May 20, 2001, (Pierre Lescanne, editor; Logic Group Preprint series No 210, Institute of Philosophy, University of Utrecht, ISBN 90-393-2764-5), pp 26-45, ps, pdf.
Implementation of Proof Search
in the Imperative Programming Language Pizza, In Proceedings
of Tableaux '98, (Springer LNAI
1397), pp 313--319, 1998. ps.gz.
L. Pinto & R. Dyckhoff, Loop-free construction of counter-models for intuitionistic propositional logic and Correction, in: Symposia Gaussiana, Conf. A, Eds.: Behara/Fritsch/Lintz, Walter de Gruyter & Co, Berlin, New York, 1995, pp 225--232.. ps.
L. Pinto & R. Dyckhoff, A constructive type system to integrate logic and functional programming, in: Proof search in type-theoretic languages (eds D. Galmiche & L. Wallen), Workshop 1B at 12th International Conference on Automated Deduction, Nancy, France, 1994, pp 70--81. ps.
R. Dyckhoff & L. Pinto, Uniform proofs and natural deductions, in: Proof search in type-theoretic languages (eds D. Galmiche & L. Wallen), Workshop 1B at 12th International Conference on Automated Deduction, Nancy, France, 1994, pp 17--23. ps.
L. Pinto, Cut formulae and logic programming, in: Extensions of Logic Programming (ed. R. Dyckhoff), Lect. Notes Art. Intell. 798, Springer-Verlag (1994), pp 282--300. ps.
R. Dyckhoff, Implementing a simple proof assistant, in: Workshop on Programming for Logic Teaching (July 1987, ed. J. Derrick and H. A. Lewis), Centre for Theoretical Computer Science, University of Leeds, Proceedings 23.88, pp 49--59. pdf.
R. Dyckhoff, Strong elimination rules in type theory, in: Workshop on Programming Logics, Marstrand (October 1987, Programming Methodology Group Report 37, ed. Nordström, Petersson and Smith), Chalmers University, Göteborg, pp 112--115. pdf.