%PDF-1.4
%
1 0 obj
<<
/Type /Catalog
/Pages 136 0 R
/Metadata 3 1 R
/Outlines 288 0 R
/Names 291 0 R
/OpenAction [ 4 0 R /Fit ]
/PageMode /UseOutlines
/ViewerPreferences << /FitWindow true >>
/PageLabels 287 0 R
>>
endobj
2 0 obj
<<
/ModDate (D:20040607094603+02'00')
/Producer (Acrobat Distiller 5.0.5 \(Windows\))
/Author (Yevgeny Kazakov and Hans de Nivelle)
/Title (LNAI 3097 - A Resolution Decision Procedure for the Guarded Fragment wit\
h Transitive Guards)
/Subject (Automated Reasoning)
/Creator (DVIPSONE \(32\) 2.1.7 http://www.YandY.com)
/CreationDate (D:20040511133644Z)
>>
endobj
3 1 obj
<< /Type /Metadata /Subtype /XML /Length 1879 >>
stream
2004-05-11T13:36:44Z
2004-06-07T09:46:03+02:00
Acrobat Distiller 5.0.5 (Windows)
DVIPSONE (32) 2.1.7 http://www.YandY.com
LNAI 3097 - A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards
Automated Reasoning
Yevgeny Kazakov and Hans de Nivelle
2004-05-11T13:36:44Z
2004-06-07T09:46:03+02:00
2004-06-07T09:46:03+02:00
Yevgeny Kazakov and Hans de Nivelle
LNAI 3097 - A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards
Automated Reasoning
LNAI 3097 - A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards
Automated Reasoning
Yevgeny Kazakov and Hans de Nivelle
endstream
endobj
4 0 obj
<<
/Type /Page
/Parent 42 0 R
/Resources 27 0 R
/Contents 26 0 R
/CropBox [ 91 90 500 750 ]
/Annots [ 21 0 R 22 0 R 23 0 R ]
>>
endobj
5 0 obj
<<
/D [ 4 0 R /XYZ null 785 null ]
/Rect [ 3391701 3765461 3523263 3633899 ]
>>
endobj
6 0 obj
<<
/Title (Introduction)
/Dest (section.1.1)
/Parent 288 0 R
/Next 7 0 R
>>
endobj
7 0 obj
<<
/Title (Preliminaries)
/Dest (section.1.2)
/Parent 288 0 R
/Prev 6 0 R
/Next 10 0 R
/First 8 0 R
/Last 9 0 R
/Count -2
>>
endobj
8 0 obj
<<
/Title (The Framework of Resolution Theorem Proving)
/Dest (subsection.1.2.1)
/Parent 7 0 R
/Next 9 0 R
>>
endobj
9 0 obj
<<
/Title (Schemes of Expressions and Clauses)
/Dest (subsection.1.2.2)
/Parent 7 0 R
/Prev 8 0 R
>>
endobj
10 0 obj
<<
/Title (Deciding the Guarded Fragment by Resolution)
/Dest (section.1.3)
/Parent 288 0 R
/Prev 7 0 R
/Next 13 0 R
/First 11 0 R
/Last 12 0 R
/Count -2
>>
endobj
11 0 obj
<<
/Title (Clause Normal Form Translation)
/Dest (subsection.1.3.1)
/Parent 10 0 R
/Next 12 0 R
>>
endobj
12 0 obj
<<
/Title (Saturation of the Clause Set)
/Dest (subsection.1.3.2)
/Parent 10 0 R
/Prev 11 0 R
>>
endobj
13 0 obj
<<
/Title (Deciding the Guarded Fragment with Transitivity)
/Dest (section.1.4)
/Parent 288 0 R
/Prev 10 0 R
/Next 17 0 R
/First 14 0 R
/Last 16 0 R
/Count -3
>>
endobj
14 0 obj
<<
/Title (Obstacles for Deciding the Guarded Fragment with Transitivity)
/Dest (subsection.1.4.1)
/Parent 13 0 R
/Next 15 0 R
>>
endobj
15 0 obj
<<
/Title (Redundancy of Inferences Involving Transitive Relations)
/Dest (subsection.1.4.2)
/Parent 13 0 R
/Prev 14 0 R
/Next 16 0 R
>>
endobj
16 0 obj
<<
/Title (Saturation of the Clause Set)
/Dest (subsection.1.4.3)
/Parent 13 0 R
/Prev 15 0 R
>>
endobj
17 0 obj
<<
/Title (Conclusions and Future Work)
/Dest (section.1.5)
/Parent 288 0 R
/Prev 13 0 R
>>
endobj
18 0 obj
<<
/D [ 4 0 R /XYZ null 769 null ]
/Rect [ 3391701 4814039 3457482 4090448 ]
>>
endobj
19 0 obj
<<
/D [ 4 0 R /XYZ null 769 null ]
/Rect [ 3391701 4814039 3457482 4090448 ]
>>
endobj
20 0 obj
<<
/D [ 4 0 R /XYZ null 557 null ]
/Rect [ 3391699 18753804 3457480 18030214 ]
>>
endobj
21 0 obj
<<
/Dest (page.136)
/Type /Annot
/Subtype /Link
/Rect [ 376 128 390 134 ]
/C [ 1 0 0 ]
/Border [ 0 0 1 ]
>>
endobj
22 0 obj
<<
/Type /Annot
/Subtype /Text
/Rect [ 605 820 623 842 ]
/Contents (Dieser Report wurde automatisch mit Hilfe der Adobe Acrobat Distiller Er\
weiterung "Distiller Secrets v1.0.5" der IMPRESSED GmbH erstellt.\rSie k\
oennen diese Startup-Datei f\374r die Distiller Versionen 4.0.5 und 5.0.\
x kostenlos unter http://www.impressed.de herunterladen.\r\rALLGEMEIN --\
--------------------------------------\rDateioptionen:\r Kompatibili\
t\344t: PDF 1.3\r F\374r schnelle Web-Anzeige optimieren: Nein\r \
Piktogramme einbetten: Nein\r Seiten automatisch drehen: Nein\r \
Seiten von: 1\r Seiten bis: Alle Seiten\r Bund: Links\r Auf\
l\366sung: [ 2400 2400 ] dpi\r Papierformat: [ 595 842 ] Punkt\r\rKO\
MPRIMIERUNG ----------------------------------------\rFarbbilder:\r \
Downsampling: Ja\r Berechnungsmethode: Bikubische Neuberechnung\r \
Downsample-Aufl\366sung: 300 dpi\r Downsampling f\374r Bilder \374\
ber: 450 dpi\r Komprimieren: Ja\r Automatische Bestimmung der Ko\
mprimierungsart: Ja\r JPEG-Qualit\344t: Maximal\r Bitanzahl pro \
Pixel: Wie Original Bit\rGraustufenbilder:\r Downsampling: Ja\r \
Berechnungsmethode: Bikubische Neuberechnung\r Downsample-Aufl\366su\
ng: 300 dpi\r Downsampling f\374r Bilder \374ber: 450 dpi\r Komp\
rimieren: Ja\r Automatische Bestimmung der Komprimierungsart: Ja\r \
JPEG-Qualit\344t: Maximal\r Bitanzahl pro Pixel: Wie Original Bit\
\rSchwarzwei\337-Bilder:\r Downsampling: Ja\r Berechnungsmethode\
: Bikubische Neuberechnung\r Downsample-Aufl\366sung: 2400 dpi\r \
Downsampling f\374r Bilder \374ber: 3600 dpi\r Komprimieren: Ja\r \
Komprimierungsart: CCITT\r CCITT-Gruppe: 4\r Graustufen gl\344\
tten: Nein\r\r Text und Vektorgrafiken komprimieren: Ja\r\rSCHRIFTEN\
----------------------------------------\r Alle Schriften einbetten\
: Ja\r Untergruppen aller eingebetteten Schriften: Nein\r Wenn E\
inbetten fehlschl\344gt: Warnen und weiter\rEinbetten:\r Immer einbe\
tten: [ /Courier-BoldOblique /Helvetica-BoldOblique /Courier /Helvetica-\
Bold /Times-Bold /Courier-Bold /Helvetica /Times-BoldItalic /Times-Roman\
/ZapfDingbats /Times-Italic /Helvetica-Oblique /Courier-Oblique /Symbol\
]\r Nie einbetten: [ ]\r\rFARBE\(N\) ------------------------------\
----------\rFarbmanagement:\r Farbumrechnungsmethode: Farbe nicht \344\
ndern\r Methode: Standard\rGer\344teabh\344ngige Daten:\r Einste\
llungen f\374r \334berdrucken beibehalten: Ja\r Unterfarbreduktion u\
nd Schwarzaufbau beibehalten: Ja\r Transferfunktionen: Anwenden\r \
Rastereinstellungen beibehalten: Ja\r\rERWEITERT ---------------------\
-------------------\rOptionen:\r Prolog/Epilog verwenden: Ja\r P\
ostScript-Datei darf Einstellungen \374berschreiben: Ja\r Level 2 co\
pypage-Semantik beibehalten: Ja\r Portable Job Ticket in PDF-Datei s\
peichern: Nein\r Illustrator-\334berdruckmodus: Ja\r Farbverl\344\
ufe zu weichen Nuancen konvertieren: Ja\r ASCII-Format: Nein\rDocume\
nt Structuring Conventions \(DSC\):\r DSC-Kommentare verarbeiten: Ja\
\r DSC-Warnungen protokollieren: Nein\r F\374r EPS-Dateien Seite\
ngr\366\337e \344ndern und Grafiken zentrieren: Ja\r EPS-Info von DS\
C beibehalten: Ja\r OPI-Kommentare beibehalten: Nein\r Dokumenti\
nfo von DSC beibehalten: Ja\r\rANDERE ----------------------------------\
------\r Distiller-Kern Version: 5000\r ZIP-Komprimierung verwen\
den: Ja\r Optimierungen deaktivieren: Nein\r Bildspeicher: 52428\
8 Byte\r Farbbilder gl\344tten: Nein\r Graustufenbilder gl\344tt\
en: Nein\r Bilder \(< 257 Farben\) in indizierten Farbraum konvertie\
ren: Ja\r sRGB ICC-Profil: sRGB IEC61966-2.1\r\rENDE DES REPORTS ---\
-------------------------------------\r\rIMPRESSED GmbH\rBahrenfelder Ch\
aussee 49\r22761 Hamburg, Germany\rTel. +49 40 897189-0\rFax +49 40 8971\
89-71\rEmail: info@impressed.de\rWeb: www.impressed.de)
/T (Verwendete Distiller 5.0.x Joboptions)
/C [ 1 1 0 ]
/Name /Note
/P 4 0 R
/NM (1900016)
/F 24
/AP << /N 297 0 R /D 299 0 R >>
>>
endobj
23 0 obj
<<
/Type /Annot
/Subtype /Text
/Rect [ 605 790 623 812 ]
/Contents (<<\r /ColorSettingsFile \(\)\r /AntiAliasMonoImages false\r \
/CannotEmbedFontPolicy /Warning\r /ParseDSCComments true\r /DoTh\
umbnails false\r /CompressPages true\r /CalRGBProfile \(sRGB IEC\
61966-2.1\)\r /MaxSubsetPct 100\r /EncodeColorImages true\r \
/GrayImageFilter /DCTEncode\r /Optimize false\r /ParseDSCComment\
sForDocInfo true\r /EmitDSCWarnings false\r /CalGrayProfile \(\)\
\r /NeverEmbed [ ]\r /GrayImageDownsampleThreshold 1.5\r /Us\
ePrologue true\r /GrayImageDict << /QFactor 0.9 /Blend 1 /HSamples [\
2 1 1 2 ] /VSamples [ 2 1 1 2 ] >>\r /AutoFilterColorImages true\r \
/sRGBProfile \(sRGB IEC61966-2.1\)\r /ColorImageDepth -1\r /\
PreserveOverprintSettings true\r /AutoRotatePages /None\r /UCRan\
dBGInfo /Preserve\r /EmbedAllFonts true\r /CompatibilityLevel 1.\
3\r /StartPage 1\r /AntiAliasColorImages false\r /CreateJobT\
icket false\r /ConvertImagesToIndexed true\r /ColorImageDownsamp\
leType /Bicubic\r /ColorImageDownsampleThreshold 1.5\r /MonoImag\
eDownsampleType /Bicubic\r /DetectBlends true\r /GrayImageDownsa\
mpleType /Bicubic\r /PreserveEPSInfo true\r /GrayACSImageDict <<\
/VSamples [ 1 1 1 1 ] /QFactor 0.15 /Blend 1 /HSamples [ 1 1 1 1 ] /Col\
orTransform 1 >>\r /ColorACSImageDict << /VSamples [ 1 1 1 1 ] /QFac\
tor 0.15 /Blend 1 /HSamples [ 1 1 1 1 ] /ColorTransform 1 >>\r /Pres\
erveCopyPage true\r /EncodeMonoImages true\r /ColorConversionStr\
ategy /LeaveColorUnchanged\r /PreserveOPIComments false\r /AntiA\
liasGrayImages false\r /GrayImageDepth -1\r /ColorImageResolutio\
n 300\r /EndPage -1\r /AutoPositionEPSFiles true\r /MonoImag\
eDepth -1\r /TransferFunctionInfo /Apply\r /EncodeGrayImages tru\
e\r /DownsampleGrayImages true\r /DownsampleMonoImages true\r \
/DownsampleColorImages true\r /MonoImageDownsampleThreshold 1.5\r \
/MonoImageDict << /K -1 >>\r /Binding /Left\r /CalCMYKProfil\
e \(U.S. Web Coated \(SWOP\) v2\)\r /MonoImageResolution 2400\r \
/AutoFilterGrayImages true\r /AlwaysEmbed [ /Courier-BoldOblique /He\
lvetica-BoldOblique /Courier /Helvetica-Bold /Times-Bold /Courier-Bold /\
Helvetica /Times-BoldItalic /Times-Roman /ZapfDingbats /Times-Italic /He\
lvetica-Oblique /Courier-Oblique /Symbol ]\r /ImageMemory 524288\r \
/SubsetFonts false\r /DefaultRenderingIntent /Default\r /OPM \
1\r /MonoImageFilter /CCITTFaxEncode\r /GrayImageResolution 300\r\
/ColorImageFilter /DCTEncode\r /PreserveHalftoneInfo true\r \
/ColorImageDict << /QFactor 0.9 /Blend 1 /HSamples [ 2 1 1 2 ] /VSample\
s [ 2 1 1 2 ] >>\r /ASCII85EncodePages false\r /LockDistillerPar\
ams false\r>> setdistillerparams\r<<\r /PageSize [ 595.276 841.890 ]\
\r /HWResolution [ 2400 2400 ]\r>> setpagedevice)
/T (Adobe Acrobat Distiller 5.0.x Joboption Datei)
/C [ 0 1 0 ]
/Name /Note
/P 4 0 R
/NM (1900017)
/F 24
/AP << /N 301 0 R /D 303 0 R >>
>>
endobj
25 0 obj
<<
/D [ 4 0 R /XYZ null null null ]
>>
endobj
26 0 obj
<< /Length 3383 /Filter /FlateDecode >>
stream
HWےܶ-'~گP%RYZ)TTԮrLr$'4eWegUn
}śȋYI^XD$YyYy*Ros8ًATمrNrUm}tېt]B$~NHjq:D:
bm'mՖYIT?ȝ$mxNA,!:qob
@Y[1A /KD_X_`8
&Iސ?<$-X*#Uʞ,p,œY1 )Z9nWƁӪ=^!7İ$j:TP7[ԛ0<,W9r3ҏ];9C5(٬sHF,QTjq:9V_6-vx[4W0VRdhģ