Ir al contenido (pulsa Retorno)

Universitat Politècnica de Catalunya

    • Català
    • Castellano
    • English
    • LoginRegisterLog in (no UPC users)
  • mailContact Us
  • world English 
    • Català
    • Castellano
    • English
  • userLogin   
      LoginRegisterLog in (no UPC users)

UPCommons. Global access to UPC knowledge

Banner header
13.560 Articles in journals published by the UPC
You are here:
View Item 
  •   DSpace Home
  • Revistes
  • Mathware & soft computing
  • 1997, Vol. IV, Núm. 2
  • View Item
  •   DSpace Home
  • Revistes
  • Mathware & soft computing
  • 1997, Vol. IV, Núm. 2
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

A reduction-based theorem prover for 3-valued logic

Thumbnail
View/Open
Aguilera.pdf (449,6Kb)
Share:
 
  View Usage Statistics
Cita com:
hdl:2099/3489

Show full item record
Aguilera Venegas, Gabriel
Pérez de Guzmán Molina, Inmaculada
Ojeda Aciego, Manuel
Document typeArticle
Defense date1997
PublisherUniversitat Politècnica de Catalunya. Secció de Matemàtiques i Informàtica
Rights accessOpen Access
Attribution-NonCommercial-NoDerivs 3.0 Spain
Except where otherwise noted, content on this work is licensed under a Creative Commons license : Attribution-NonCommercial-NoDerivs 3.0 Spain
Abstract
We present a new prover for propositional 3-valued logics, TAS-M3, which is an extension of the TAS-D prover for classical propositional logic. TAS-M3 uses the TAS methodology and, consequently, it is a {\em reduction-based\/} method. Thus, its power is based on the reductions of the size of the formula executed by the $\efe$ transformation. This transformation dynamically "filters" the information contained in the syntactic structure of the formula to avoid as much distributions (of $\land$ wrt $\lor$ in our case) as possible, in order to improve efficiency. In our opinion, this filtering is the key of the TAS methodology which, as shown in this paper, allows the method to be extremely adaptable, because switching to different kinds of logic is possible without having to redesign the whole prover.
URIhttp://hdl.handle.net/2099/3489
ISSN1134-5632
Collections
  • Mathware & soft computing - 1997, Vol. IV, Núm. 2 [5]
Share:
 
  View Usage Statistics

Show full item record

FilesDescriptionSizeFormatView
Aguilera.pdf449,6KbPDFView/Open

Browse

This CollectionBy Issue DateAuthorsOther contributionsTitlesSubjectsThis repositoryCommunities & CollectionsBy Issue DateAuthorsOther contributionsTitlesSubjects

© UPC Obrir en finestra nova . Servei de Biblioteques, Publicacions i Arxius

info.biblioteques@upc.edu

  • About This Repository
  • Contact Us
  • Send Feedback
  • Privacy Settings
  • Inici de la pàgina