dc.date.accessioned 2013-03-12T07:57:19Z dc.date.available 2013-03-12T07:57:19Z dc.date.issued 2005 en_US dc.date.submitted 2005-06-10 en_US dc.identifier.citation Holen, Bjarne. A Reflective Theorem Prover for the Connection Calculus. Masteroppgave, University of Oslo, 2005 en_US dc.identifier.uri http://hdl.handle.net/10852/9285 dc.description.abstract Rewriting logic can be used to prototype systems for automated deduction. In this paper, we illustrate how this approach allows experiments with deduction strategies in a flexible and conceptually satisfying way. This is achieved by exploiting the reflective property of rewriting logic. By specifying a theorem prover in this way one quickly obtains a readable, reliable and reasonably efficient system which can be used both as a platform for tactic experiments and as a basis for an optimized implementation. The approach is illustrated by specifying a calculus for the connection method in rewriting logic which clearly separates rules from tactics. nor dc.language.iso eng en_US dc.title A Reflective Theorem Prover for the Connection Calculus en_US dc.type Master thesis en_US dc.date.updated 2005-07-25 en_US dc.creator.author Holen, Bjarne en_US dc.subject.nsi VDP::420 en_US dc.identifier.bibliographiccitation info:ofi/fmt:kev:mtx:ctx&ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:dissertation&rft.au=Holen, Bjarne&rft.title=A Reflective Theorem Prover for the Connection Calculus&rft.inst=University of Oslo&rft.date=2005&rft.degree=Masteroppgave en_US dc.identifier.urn URN:NBN:no-10624 en_US dc.type.document Masteroppgave en_US dc.identifier.duo 28063 en_US dc.contributor.supervisor Arild Waaler, Einar Broch Johnsen en_US dc.identifier.bibsys 05136932x en_US dc.identifier.fulltext Fulltext https://www.duo.uio.no/bitstream/handle/10852/9285/1/thesis2.pdf
﻿