dc.date.accessioned | 2013-03-12T08:05:09Z | |
dc.date.available | 2013-03-12T08:05:09Z | |
dc.date.issued | 2009 | en_US |
dc.date.submitted | 2009-05-14 | en_US |
dc.identifier.citation | Thorstensen, Evgenij. Instance-Based Hyper-Tableaux for Coherent Logic. Masteroppgave, University of Oslo, 2009 | en_US |
dc.identifier.uri | http://hdl.handle.net/10852/10073 | |
dc.description.abstract | We consider a fragment of first-order logic known as coherent logic or geometric logic. The essential difference to standard clausal form is that there may be existentially quantified variables in the positive literals of a clause, and only constants and variables are allowed as terms. Coherent logic is interesting because many problems naturally fall into the fragment. Furthermore, the simple term structure might allow for efficient implementations. We propose a calculus for this fragment that extends the `next-generation' hyper-tableaux calculus of Baumgartner, and prove it sound and complete. To our knowledge, this is the first instance-based method that works on a richer input than clause normal form. | eng |
dc.language.iso | eng | en_US |
dc.title | Instance-Based Hyper-Tableaux for Coherent Logic | en_US |
dc.type | Master thesis | en_US |
dc.date.updated | 2009-09-07 | en_US |
dc.creator.author | Thorstensen, Evgenij | 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=Thorstensen, Evgenij&rft.title=Instance-Based Hyper-Tableaux for Coherent Logic&rft.inst=University of Oslo&rft.date=2009&rft.degree=Masteroppgave | en_US |
dc.identifier.urn | URN:NBN:no-22666 | en_US |
dc.type.document | Masteroppgave | en_US |
dc.identifier.duo | 91821 | en_US |
dc.contributor.supervisor | Martin Giese, Arild Waaler | en_US |
dc.identifier.bibsys | 09320177x | en_US |
dc.identifier.fulltext | Fulltext https://www.duo.uio.no/bitstream/handle/10852/10073/2/Thorstensen.pdf | |