@INPROCEEDINGS{Georgieva+Hustadt+Schmidt@FTP2000,
 AUTHOR        = {Georgieva, Lilia and Hustadt, Ullrich and Schmidt, Renate A.},
 TITLE         = {Hyperresolution for Guarded Formulae},
 PAGES         = {101-112},
 YEAR          = {2000},
 BOOKTITLE     = {Proceedings of the Third International Workshop on 
 First-Order Theorem Proving (FTP 2000) [St. Andrews, Scotland, 2-4 July 2000]},
 EDITOR        = {Baumgartner, Peter and Zhang, Hantao},
 PUBLISHER     = {Institut f{\"u}r Informatik, Universit{\"a}t Koblenz-Landau},
 PADDRESS      = {Koblenz, Germany},
 PYEAR         = {2000},
 CADDRESS      = {St. Andrews, Scotland},
 CYEAR         = {2000},
 CMONTH        = jul # {~3--5},
 SERIES        = {Fachberichte Informatik},
 VOLUME        = {5/2000},
 URL           = {Georgieva+Hustadt+Schmidt@FTP2000.pdf},
 ABSTRACT      = {This paper investigates the use of hyperresolution
 as a decision procedure and model builder for guarded formulae. In
 general hyperresolution is not a decision procedure for the entire
 guarded fragment. However we show that there are natural fragements
 which can be decided by hyperresolution. In particular, we prove
 decidability of hyperresolution with or without splitting for the
 fragment GF1- and point out several ways of extending this fragment
 without loosing decidability. As hyperresolution is closely related to
 various tableaux methods the present work is also relevant for
 tableaux methods. We compare our approach to hypertableaux, and
 mention the relationship to other clausal classes which are decidable
 by hyperresolution.}
}

{"_id":"AezCHCtk8uatz6xWo","bibbaseid":"georgieva-hustadt-schmidt-hyperresolutionforguardedformulae-2000","author_short":["Georgieva, L.","Hustadt, U.","Schmidt, R. A."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Georgieva"],"firstnames":["Lilia"],"suffixes":[]},{"propositions":[],"lastnames":["Hustadt"],"firstnames":["Ullrich"],"suffixes":[]},{"propositions":[],"lastnames":["Schmidt"],"firstnames":["Renate","A."],"suffixes":[]}],"title":"Hyperresolution for Guarded Formulae","pages":"101-112","year":"2000","booktitle":"Proceedings of the Third International Workshop on First-Order Theorem Proving (FTP 2000) [St. Andrews, Scotland, 2-4 July 2000]","editor":[{"propositions":[],"lastnames":["Baumgartner"],"firstnames":["Peter"],"suffixes":[]},{"propositions":[],"lastnames":["Zhang"],"firstnames":["Hantao"],"suffixes":[]}],"publisher":"Institut für Informatik, Universität Koblenz-Landau","paddress":"Koblenz, Germany","pyear":"2000","caddress":"St. Andrews, Scotland","cyear":"2000","cmonth":"July 3–5","series":"Fachberichte Informatik","volume":"5/2000","url":"Georgieva+Hustadt+Schmidt@FTP2000.pdf","abstract":"This paper investigates the use of hyperresolution as a decision procedure and model builder for guarded formulae. In general hyperresolution is not a decision procedure for the entire guarded fragment. However we show that there are natural fragements which can be decided by hyperresolution. In particular, we prove decidability of hyperresolution with or without splitting for the fragment GF1- and point out several ways of extending this fragment without loosing decidability. As hyperresolution is closely related to various tableaux methods the present work is also relevant for tableaux methods. We compare our approach to hypertableaux, and mention the relationship to other clausal classes which are decidable by hyperresolution.","bibtex":"@INPROCEEDINGS{Georgieva+Hustadt+Schmidt@FTP2000,\n AUTHOR = {Georgieva, Lilia and Hustadt, Ullrich and Schmidt, Renate A.},\n TITLE = {Hyperresolution for Guarded Formulae},\n PAGES = {101-112},\n YEAR = {2000},\n BOOKTITLE = {Proceedings of the Third International Workshop on \n First-Order Theorem Proving (FTP 2000) [St. Andrews, Scotland, 2-4 July 2000]},\n EDITOR = {Baumgartner, Peter and Zhang, Hantao},\n PUBLISHER = {Institut f{\\\"u}r Informatik, Universit{\\\"a}t Koblenz-Landau},\n PADDRESS = {Koblenz, Germany},\n PYEAR = {2000},\n CADDRESS = {St. Andrews, Scotland},\n CYEAR = {2000},\n CMONTH = jul # {~3--5},\n SERIES = {Fachberichte Informatik},\n VOLUME = {5/2000},\n URL = {Georgieva+Hustadt+Schmidt@FTP2000.pdf},\n ABSTRACT = {This paper investigates the use of hyperresolution\n as a decision procedure and model builder for guarded formulae. In\n general hyperresolution is not a decision procedure for the entire\n guarded fragment. However we show that there are natural fragements\n which can be decided by hyperresolution. In particular, we prove\n decidability of hyperresolution with or without splitting for the\n fragment GF1- and point out several ways of extending this fragment\n without loosing decidability. As hyperresolution is closely related to\n various tableaux methods the present work is also relevant for\n tableaux methods. We compare our approach to hypertableaux, and\n mention the relationship to other clausal classes which are decidable\n by hyperresolution.}\n}\n","author_short":["Georgieva, L.","Hustadt, U.","Schmidt, R. A."],"editor_short":["Baumgartner, P.","Zhang, H."],"key":"Georgieva+Hustadt+Schmidt@FTP2000","id":"Georgieva+Hustadt+Schmidt@FTP2000","bibbaseid":"georgieva-hustadt-schmidt-hyperresolutionforguardedformulae-2000","role":"author","urls":{"Paper":"http://cgi.csc.liv.ac.uk/~ullrich/publications/Georgieva+Hustadt+Schmidt@FTP2000.pdf"},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"http://cgi.csc.liv.ac.uk/~ullrich/publications/all.bib?authorFirst=1","dataSources":["WhiGijHmCtTSdLaAj","FgmYE34DdKWThg2dR"],"keywords":[],"search_terms":["hyperresolution","guarded","formulae","georgieva","hustadt","schmidt"],"title":"Hyperresolution for Guarded Formulae","year":2000}