@INPROCEEDINGS{Ludwig+Hustadt@TIME2009,
 AUTHOR        = {Ludwig, Michel and Hustadt, Ullrich},
 TITLE         = {Resolution-Based Model Construction for {PLTL}},
 BOOKTITLE     = {Proceedings of the 16th International Symposium on
 Temporal Representation and Reasoning (TIME-2009)
 [Brixen-Bressanone, Italy, 23-25 July 2009]},
 YEAR          = {2009},
 EDITOR        = {Lutz, Carsten and Raskin, Jean-Francois},
 PAGES         = {73-80},
 PUBLISHER     = {IEEE Computer Society},
 CADDRESS      = {Brixen-Bressanone, Italy},
 CYEAR         = {2009},
 CMONTH        = jul # {23--25},
 YEAR          = {2009},
 URL           = {Ludwig+Hustadt@TIME2009.pdf},
 ABSTRACT = {The elimination of redundant clauses is an essential part
 of resolution-based theorem proving in order to reduce the size of
 the search space. In this paper we focus on ordered fine-grained
 resolution with selection, a sound and complete resolution-based
 calculus for monodic first-order temporal logic. The inference rules
 of the calculus are based on standard resolution between different
 types of temporal clauses on one hand and inference rules with
 semi-decidable applicability conditions that handle eventualities on
 the other hand. We define a subsumption relation on temporal clauses
 and show how the calculus can be extended with reduction rules that
 eliminate redundant clauses. We also illustrate how the subsumption
 relation can be used to simplify the loop search process for
 eventualities.}
}

{"_id":"ScHnPpxawLFyDAbu8","bibbaseid":"ludwig-hustadt-resolutionbasedmodelconstructionforpltl-2009","author_short":["Ludwig, M.","Hustadt, U."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Ludwig"],"firstnames":["Michel"],"suffixes":[]},{"propositions":[],"lastnames":["Hustadt"],"firstnames":["Ullrich"],"suffixes":[]}],"title":"Resolution-Based Model Construction for PLTL","booktitle":"Proceedings of the 16th International Symposium on Temporal Representation and Reasoning (TIME-2009) [Brixen-Bressanone, Italy, 23-25 July 2009]","year":"2009","editor":[{"propositions":[],"lastnames":["Lutz"],"firstnames":["Carsten"],"suffixes":[]},{"propositions":[],"lastnames":["Raskin"],"firstnames":["Jean-Francois"],"suffixes":[]}],"pages":"73-80","publisher":"IEEE Computer Society","caddress":"Brixen-Bressanone, Italy","cyear":"2009","cmonth":"July23–25","url":"Ludwig+Hustadt@TIME2009.pdf","abstract":"The elimination of redundant clauses is an essential part of resolution-based theorem proving in order to reduce the size of the search space. In this paper we focus on ordered fine-grained resolution with selection, a sound and complete resolution-based calculus for monodic first-order temporal logic. The inference rules of the calculus are based on standard resolution between different types of temporal clauses on one hand and inference rules with semi-decidable applicability conditions that handle eventualities on the other hand. We define a subsumption relation on temporal clauses and show how the calculus can be extended with reduction rules that eliminate redundant clauses. We also illustrate how the subsumption relation can be used to simplify the loop search process for eventualities.","bibtex":"@INPROCEEDINGS{Ludwig+Hustadt@TIME2009,\n AUTHOR = {Ludwig, Michel and Hustadt, Ullrich},\n TITLE = {Resolution-Based Model Construction for {PLTL}},\n BOOKTITLE = {Proceedings of the 16th International Symposium on\n Temporal Representation and Reasoning (TIME-2009)\n [Brixen-Bressanone, Italy, 23-25 July 2009]},\n YEAR = {2009},\n EDITOR = {Lutz, Carsten and Raskin, Jean-Francois},\n PAGES = {73-80},\n PUBLISHER = {IEEE Computer Society},\n CADDRESS = {Brixen-Bressanone, Italy},\n CYEAR = {2009},\n CMONTH = jul # {23--25},\n YEAR = {2009},\n URL = {Ludwig+Hustadt@TIME2009.pdf},\n ABSTRACT = {The elimination of redundant clauses is an essential part\n of resolution-based theorem proving in order to reduce the size of\n the search space. In this paper we focus on ordered fine-grained\n resolution with selection, a sound and complete resolution-based\n calculus for monodic first-order temporal logic. The inference rules\n of the calculus are based on standard resolution between different\n types of temporal clauses on one hand and inference rules with\n semi-decidable applicability conditions that handle eventualities on\n the other hand. We define a subsumption relation on temporal clauses\n and show how the calculus can be extended with reduction rules that\n eliminate redundant clauses. We also illustrate how the subsumption\n relation can be used to simplify the loop search process for\n eventualities.}\n}\n","author_short":["Ludwig, M.","Hustadt, U."],"editor_short":["Lutz, C.","Raskin, J."],"key":"Ludwig+Hustadt@TIME2009","id":"Ludwig+Hustadt@TIME2009","bibbaseid":"ludwig-hustadt-resolutionbasedmodelconstructionforpltl-2009","role":"author","urls":{"Paper":"http://cgi.csc.liv.ac.uk/~ullrich/publications/Ludwig+Hustadt@TIME2009.pdf"},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"http://cgi.csc.liv.ac.uk/~ullrich/publications/all.bib?authorFirst=1","dataSources":["WhiGijHmCtTSdLaAj"],"keywords":[],"search_terms":["resolution","based","model","construction","pltl","ludwig","hustadt"],"title":"Resolution-Based Model Construction for PLTL","year":2009}