b'@inproceedings{SudaWeidenbachIJCAR2012,'b'\nTITLE = {A {PLTL}-Prover Based on Labelled Superposition with Partial Model Guidance},\nAUTHOR = {Suda, Martin and Weidenbach, Christoph},\nLANGUAGE = {eng},\nISSN = {0302-9743},\nISBN = {978-3-642-31364-6},\nDOI = {10.1007/978-3-642-31365-3_42},\nLOCALID = {Local-ID: BED98A2F132CC156C1257AD10038A23D-SudaWeidenbachIJCAR2012},\nPUBLISHER = {Springer},\nYEAR = {2012},\nDATE = {2012},\nABSTRACT = {Labelled superposition (LPSup) is a new calculus for PLTL. One of its distinguishing features, in comparison to other resolution-based approaches, is its ability to construct partial models on the fly. We use this feature to design a new decision procedure for the logic, where the models are effectively used to guide the search. On a representative set of benchmarks, our implementation is then shown to considerably advance the state of the art.},\nBOOKTITLE = {Automated Reasoning (IJCAR 2012)},\nEDITOR = {Gramlich, Bernhard and Miller, Dale and Sattler, Uli},\nPAGES = {537--543},\nSERIES = {Lecture Notes in Artificial Intelligence},\nVOLUME = {7364},\nADDRESS = {Manchester, UK},\n}\n'