A term rewriting technique for decision graphs

dc.contributor.authorBadban, Bahareh
dc.date.accessioned2011-03-24T16:09:07Zdeu
dc.date.available2011-06-30T22:25:05Zdeu
dc.date.issued2009deu
dc.description.abstractWe provide an automatic verification for a fragment of FOL quantifier-free logic with zero, successor and equality. We use BDD representation of such formulas and to verify them, we first introduce a (complete) term rewrite system to generate an equivalent Ordered (0, S,=)-BDD from any given (0, S,=)-BDD. Having the ordered representation of the BDDs, one can verify the original formula in constant time. Then, to have this transformation automatically, we provide an algorithm which will do the whole process.eng
dc.description.versionpublished
dc.format.mimetypeapplication/pdfdeu
dc.identifier.citationPaper presented at: The International Workshop on Computing with Terms and Graphs 9 (2009)deu
dc.identifier.ppn318538350deu
dc.identifier.urihttp://kops.uni-konstanz.de/handle/123456789/6064
dc.language.isoengdeu
dc.legacy.dateIssued2010deu
dc.rightsterms-of-usedeu
dc.rights.urihttps://rightsstatements.org/page/InC/1.0/deu
dc.subjectTerm Rewrite Systemdeu
dc.subjectFirst-Order Logicdeu
dc.subjectDecision Proceduredeu
dc.subjectVerificationdeu
dc.subject.ddc004deu
dc.titleA term rewriting technique for decision graphseng
dc.typeINPROCEEDINGSdeu
dspace.entity.typePublication
kops.citation.bibtex
@inproceedings{Badban2009rewri-6064,
  year={2009},
  title={A term rewriting technique for decision graphs},
  booktitle={The International Workshop on Computing with Terms and Graphs 9},
  author={Badban, Bahareh}
}
kops.citation.iso690BADBAN, Bahareh, 2009. A term rewriting technique for decision graphs. In: The International Workshop on Computing with Terms and Graphs 9. 2009deu
kops.citation.iso690BADBAN, Bahareh, 2009. A term rewriting technique for decision graphs. In: The International Workshop on Computing with Terms and Graphs 9. 2009eng
kops.citation.rdf
<rdf:RDF
    xmlns:dcterms="http://purl.org/dc/terms/"
    xmlns:dc="http://purl.org/dc/elements/1.1/"
    xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
    xmlns:bibo="http://purl.org/ontology/bibo/"
    xmlns:dspace="http://digital-repositories.org/ontologies/dspace/0.1.0#"
    xmlns:foaf="http://xmlns.com/foaf/0.1/"
    xmlns:void="http://rdfs.org/ns/void#"
    xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > 
  <rdf:Description rdf:about="https://kops.uni-konstanz.de/server/rdf/resource/123456789/6064">
    <dcterms:title>A term rewriting technique for decision graphs</dcterms:title>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:09:07Z</dc:date>
    <dcterms:abstract xml:lang="eng">We provide an automatic verification for a fragment of FOL quantifier-free logic with zero, successor and equality. We use BDD representation of such formulas and to verify them, we first introduce a (complete) term rewrite system to generate an equivalent Ordered (0, S,=)-BDD from any given (0, S,=)-BDD. Having the ordered representation of the BDDs, one can verify the original formula in constant time. Then, to have this transformation automatically, we provide an algorithm which will do the whole process.</dcterms:abstract>
    <dcterms:bibliographicCitation>Paper presented at: The International Workshop on Computing with Terms and Graphs 9 (2009)</dcterms:bibliographicCitation>
    <dc:contributor>Badban, Bahareh</dc:contributor>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/6064/1/A_Term_Rewriting_Technique_2009_KOPS10598.pdf"/>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dc:format>application/pdf</dc:format>
    <dc:rights>terms-of-use</dc:rights>
    <dc:language>eng</dc:language>
    <dcterms:issued>2009</dcterms:issued>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-06-30T22:25:05Z</dcterms:available>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/6064/1/A_Term_Rewriting_Technique_2009_KOPS10598.pdf"/>
    <dc:creator>Badban, Bahareh</dc:creator>
    <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/6064"/>
  </rdf:Description>
</rdf:RDF>
kops.description.openAccessopenaccessgreen
kops.identifier.nbnurn:nbn:de:bsz:352-opus-105985deu
kops.opus.id10598deu
kops.sourcefield<i>The International Workshop on Computing with Terms and Graphs 9</i>. 2009deu
kops.sourcefield.plainThe International Workshop on Computing with Terms and Graphs 9. 2009deu
kops.sourcefield.plainThe International Workshop on Computing with Terms and Graphs 9. 2009eng
relation.isAuthorOfPublication7836390d-fc5b-4523-a272-2f8f5025bf3f
relation.isAuthorOfPublication.latestForDiscovery7836390d-fc5b-4523-a272-2f8f5025bf3f
source.titleThe International Workshop on Computing with Terms and Graphs 9eng

Dateien

Originalbündel

Gerade angezeigt 1 - 1 von 1
Vorschaubild nicht verfügbar
Name:
A_Term_Rewriting_Technique_2009_KOPS10598.pdf
Größe:
150.18 KB
Format:
Adobe Portable Document Format
A_Term_Rewriting_Technique_2009_KOPS10598.pdf
A_Term_Rewriting_Technique_2009_KOPS10598.pdfGröße: 150.18 KBDownloads: 232