%%% ==================================================================== %%% BibTeX-file{ %%% author = "Cesare Tinelli", %%% date = "17 Aug 2005", %%% filename = "TinelliC.bib", %%% url = "ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/TinelliC.bib", %%% www-home = "http://www.cs.uiowa.edu/~tinelli/", %%% address = "Department of Computer Science, %%% The University of Iowa, %%% 14 MacLean Hall, %%% Iowa City, Iowa 52242, USA", %%% telephone = "+1-319-335-0735", %%% FAX = "+1-319-335-3624", %%% email = "tinelli at cs dot uiowa dot edu", %%% dates = {1996--}, %%% keywords = "combination methods, decision procedures, automated reasoning, satisfiability modulo theories", %%% supported = "yes", %%% supported-by = "Cesare Tinelli", %%% abstract = "Bibliography for Cesare Tinelli" %%% } %%% ==================================================================== @Article{BaaGT-IC-06, author = {Franz Baader and Silvio Ghilardi and Cesare Tinelli}, title = {A new combination procedure for the word problem that generalizes fusion decidability results in modal logics}, journal = {Information and Computation}, year = 2005, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, OPTnote = {(Accepted for publication.)}, } @TECHREPORT{Tin-SMTLIB-05, author = {Silvio Ranise and Cesare Tinelli}, title = {The SMT-LIB Standard: Version 1.1}, year = 2005, } @Article{TinZar-JAR-05, author = {Cesare Tinelli and Calogero Zarba}, title = {Combining non-stably infinite theories}, journal = {Journal of Automated Reasoning}, year = 2005, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, note = {(To appear.)}, } @InProceedings{BauTin-CADE-05, author = {Peter Baumgartner and Cesare Tinelli}, title = {The Model Evolution Calculus with Equality}, booktitle = {Proceedings of the 20th International Conference on Automated Deduction, CADE-20 (Tallinn, Estonia)}, year = 2005, editor = {R.~Nieuwenhuis}, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, number = {3632}, pages = {392--408}, url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/BauTin-CADE-05.pdf}, } @Article{BauFT-IJAIT-05, author = {Peter Baumgartner, Alexander Fuchs and Cesare Tinelli}, title = {Implementing Model Evolution Calculus}, journal = {International Journal of Artificial Intelligence Tools}, year = 2005, note = {(Accepted for publication.)}, url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/BauFT-IJAIT-05.pdf}, } @Proceedings{Ahrendt:etal:DisprovingAndPDPAR:ENTCS:05, title = {{S}elected {P}apers from the {W}orkshops on {D}isproving and the {S}econd {I}nternational {W}orkshop on {P}ragmatics of {D}ecision {P}rocedures ({PDPAR} 2004)}, booktitle = {{S}elected {P}apers from the {W}orkshops on {D}isproving and the {S}econd {I}nternational {W}orkshop on {P}ragmatics of {D}ecision {P}rocedures ({PDPAR} 2004)}, editor = {Wolfgang Ahrendt and Peter Baumgartner and Hans de Nivelle and Silvio Ranise and Cesare Tinelli}, year = {2005}, volume = {125}, number = {3}, pages = {1--164}, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier}, } @InProceedings{NieOT-LPAR-04, author = {Robert Nieuwenhuis and Albert Oliveras and Cesare Tinelli}, title = {Abstract {DPLL} and Abstract {DPLL} Modulo Theories}, booktitle = {Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'04), Montevideo, Uruguay}, pages = {36--50}, year = 2005, editor = {F.~Baader and A.~Voronkov}, volume = 3452, series = {Lecture Notes in Computer Science}, publisher = {Springer}, url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/NieOT-LPAR-04.pdf}, } @InProceedings{TinZar-JELIA-04, author = {Cesare Tinelli and Calogero Zarba}, title = {Combining decision procedures for sorted theories}, booktitle = {Proceedings of the 9th European Conference on Logic in Artificial Intelligence (JELIA'04), Lisbon, Portugal}, pages = {641--653}, year = 2004, editor = {J.~Alferes and J.~Leite}, volume = 3229, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/TinZar-JELIA-04.pdf} } @InProceedings{BauFT-ESFOR-04, author = {Peter Baumgartner, Alexander Fuchs and Cesare Tinelli}, title = {Darwin: A Theorem Prover for the Model Evolution Calculus}, booktitle = {Proceedings of the 1st Workshop on Empirically Successful First Order Reasoning (ESFOR'04), Cork, Ireland, 2004}, year = 2004, editor = {G.~Sutcliffe and S.~Schultz and T.~Tammet}, OPTvolume = {}, OPTnumber = {}, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier}, url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/BauFT-ESFOR-04.pdf} } @InProceedings{GanHNOT-CAV-04, author = {Harald Ganzinger and George Hagen and Robert Nieuwenhuis and Albert Oliveras and Cesare Tinelli}, title = {{DPLL(T)}: Fast Decision Procedures}, booktitle = {Proceedings of the 16th International Conference on Computer Aided Verification, CAV'04 (Boston, Massachusetts)}, pages = {175-188}, year = 2004, editor = {R.~Alur and D.~Peled}, volume = 3114, series = {Lecture Notes in Computer Science}, publisher = {Springer}, url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/GanHNOT-CAV-04.pdf}, } @InProceedings{BaaGT-IJCAR-04, author = {Franz Baader and Silvio Ghilardi and Cesare Tinelli}, title = {A new combination procedure for the word problem that generalizes fusion decidability results in modal logics}, booktitle = {Proceedings of the 2nd International Joint Conference on Automated Reasoning, IJCAR'04, (Cork, Ireland)}, pages = {183-197}, year = 2004, editor = {D.~Basin and M.~Rusinowitch}, volume = 3097, series = {Lecture Notes in Computer Science}, publisher = {Springer}, url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/BaaGT-IJCAR-04.pdf} } @InProceedings{BauTin-CADE-03, author = {Peter Baumgartner and Cesare Tinelli}, title = {The Model Evolution Calculus}, booktitle = {Proceedings of the 19th International Conference on Automated Deduction, CADE-19 (Miami, Florida, USA)}, year = 2003, editor = {F.~Baader}, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, number = 2741, pages = {350-364}, url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/BauTin-CADE-03.pdf}, } @InProceedings{TinZar-FTP-03, author = {Cesare Tinelli and Calogero Zarba}, title = {Combining non-stably infinite theories}, booktitle = {Proceedings of the 4th International Workshop on First Order Theorem Proving, FTP'03 (Valencia, Spain)}, editor = {I.~Dahn and L.~Vigneron}, year = 2003, series = {Electronic Notes in Theoretical Computer Science}, volume = {86.1}, publisher = {Elsevier Science Publishers}, } @TECHREPORT{TinZar-RR-03, author = {Cesare Tinelli and Calogero Zarba}, title = {Combining non-stably infinite theories}, institution = {Department of Computer Science, The University of Iowa}, number = {03-01}, month = Apr, year = 2003, url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/TinZar-RR-03.pdf}, } @TechReport{BauTin-RR-03, author = {Peter Baumgartner and Cesare Tinelli}, title = {The Model Evolution Calculus}, institution = {Universit{\"a}t Koblenz-Landau}, year = 2003, type = {Fachberichte Informatik}, number = {1/2003}, address = {Institut f{\"u}r Informatik, Universit{\"a}t Koblenz-Landau}, url = "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-1-2003.pdf" , } @Article{Tin-JAR-03, author = {Cesare Tinelli}, title = {Cooperation of Background Reasoners in Theory Reasoning by Residue Sharing}, journal = {Journal of Automated Reasoning}, volume = 30, number = 1, pages = {1-31}, month = jan, year = 2003, url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/Tin-JAR-03.pdf}, } @Article{TinRin-TCS-03, author = {Cesare Tinelli and Christophe Ringeissen}, title = {Unions of Non-Disjoint Theories and Combinations of Satisfiability Procedures}, journal = {Theoretical Computer Science}, month = jan, volume = 290, number = 1, year = 2003, pages = {291--353}, url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/TinRin-TCS-03.pdf}, } @Article{BaaTin-IC-02, author = {Franz Baader and Cesare Tinelli}, title = {Deciding the Word Problem in the Union of equational Theories}, journal = {Information and Computation}, volume = 178, number = 2, month = dec, year = 2002, pages = {346--390}, url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/BaaTin-IC-02.pdf}, } @InProceedings{Tin-JELIA-02, author = {Cesare Tinelli}, title = {A {DPLL}-based Calculus for Ground Satisfiability Modulo Theories}, booktitle = {Proceedings of the 8th European Conference on Logics in Artificial Intelligence (Cosenza, Italy)}, year = 2002, editor = {Giovambattista Ianni and Sergio Flesca}, volume = 2424, pages = {308-319}, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/Tin-JELIA-02.pdf}, } @TECHREPORT{Tin-RR-02, author = {Cesare Tinelli}, title = {Cooperation of Background Reasoners in Theory Reasoning by Residue Sharing}, institution = {Department of Computer Science, University of Iowa}, month = may, number = {02-03}, year = 2002, url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/Tin-RR-02.pdf}, } @INPROCEEDINGS{BaaTin-RTA-02, author = {Franz Baader and Cesare Tinelli}, title = {Combining Decision Procedures for Positive Theories Sharing Constructors.}, editor = {S.~Tison}, booktitle = {Proceedings of the 13th International Conference on Rewriting Techniques and Applications (Copenhagen, Denmark)}, volume = 2378, year = 2002, publisher = {Springer}, series = {Lecture Notes in Computer Science}, pages = {352--366}, url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/BaaTin-RTA-02.pdf}, } @TECHREPORT{BaaTin-RR-02, author = {Franz Baader and Cesare Tinelli}, title = {Combining Decision Procedures for Positive Theories Sharing Constructors}, institution = {Department of Computer Science, University of Iowa}, month = Feb, year = 2002, number = {02-02}, url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/BaaTin-RR-02.pdf}, } @TECHREPORT{TinRin-RR-01, author = {Cesare Tinelli and Christophe Ringeissen}, title = {Unions of Non-Disjoint Theories and Combinations of Satisfiability Procedures}, institution = {Department of Computer Science, University of Iowa}, month = apr, year = 2001, number = {01-02}, url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/TinRin-RR-01.pdf}, } @InProceedings{Tin-FTP-00, author = {Cesare Tinelli}, editor = {Peter Baumgartner and Hantao Zhang}, title = {Cooperation of Background Reasoners in Theory Reasoning by Residue Sharing}, booktitle = {International Workshop on First Order Theorem Proving, FTP'2000, St Andrews (Scotland)}, month = jul, year = 2000, publisher = {University of Koblenz}, url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/Tin-FTP-00.pdf}, } @INPROCEEDINGS{BaaTin-FROCOS-00, author = {Franz Baader and Cesare Tinelli}, title = {Combining Equational Theories Sharing Non-Collapse-Free Constructors}, editor = {H.~Kirchner and Ch.~Ringeissen}, booktitle = {Proceedings of the 3rd International Workshop on Frontiers of Combining Systems, {FroCoS'2000}, Nancy (France)}, series = {Lecture Notes in Artificial Intelligence}, volume = 1794, publisher = {Springer-Verlag}, month = mar, year = 2000, pages = {260-274}, url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/BaaTin-RTA-99.pdf}, } @TECHREPORT{BaaTin-RR-99, author = {Franz Baader and Cesare Tinelli}, title = {Combining Equational Theories Sharing Non-Collapse-Free Constructors}, institution = {Department of Computer Science, University of Iowa}, month = oct, year = 1999, number = {99-13}, url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/BaaTin-RR-99.pdf}, } @INPROCEEDINGS{BaaTin-RTA-99, author = {Franz Baader and Cesare Tinelli}, title = {Deciding the Word Problem in the Union of Equational Theories Sharing Constructors}, editor = {P.~Narendran and M.~Rusinowitch}, booktitle = {Proceedings of the 10th International Conference on Rewriting Techniques and Applications (Trento, Italy)}, year = 1999, publisher = {Springer-Verlag}, volume = 1631, pages = {175--189}, series = {Lecture Notes in Computer Science}, url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/}, } @PHDTHESIS{Tin-PHD-99, author = {Cesare Tinelli}, title = {Combination of Decidability Procedures for Automated Deduction and Constraint-Based Reasoning}, type = {{PhD} Dissertation}, school = {Department of Computer Science, University of Illinois at Urbana-Champaign}, month = may, year = 1999, address = {Urbana-Champaign, Illinois}, url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/Tin-PHD-99.pdf}, } @ARTICLE{TinHar-JFLP-98, author = {Cesare Tinelli and Mehdi T. Harandi}, title = {Constraint Logic Programming over Unions of Constraint Theories}, journal = {The Journal of Functional and Logic Programming}, month = dec, year = 1998, volume = 1998, number = 6, publisher = {The MIT Press}, url = {ftp://mitpress.mit.edu/pub/JFLP/JFLP1998/A98-06/JFLP-A98-06.ps}, } @TECHREPORT{BaaTin-RR-98, author = {Franz Baader and Cesare Tinelli}, title = {Deciding the Word Problem in the Union of Equational Theories}, institution = {Department of Computer Science, University of Illinois at Urbana-Champaign}, month = oct, year = 1998, number = {UIUCDCS-R-98-2073}, url = {http://www.cs.uiuc.edu/Dienst/UI/2.0/Describe/ncstrl.uiuc_cs/UIUCDCS-R-98-2073}, } @TECHREPORT{TinRin-RR-98, author = {Cesare Tinelli and Christophe Ringeissen}, title = {Non-Disjoint Unions of Theories and Combinations of Satisfiability Procedures: First Results}, institution = {Department of Computer Science, University of Illinois at Urbana-Champaign}, month = apr, year = 1998, number = {UIUCDCS-R-98-2044}, note = {(also available as INRIA research report no. RR-3402)}, url = {http://www.cs.uiuc.edu/Dienst/UI/2.0/Describe/ncstrl.uiuc_cs/UIUCDCS-R-98-2044}, } @INPROCEEDINGS{BaaTin-CADE-97, author = {Franz Baader and Cesare Tinelli}, title = {A New Approach for Combining Decision Procedures for the Word Problem, and Its Connection to the {N}elson-{O}ppen Combination Method}, editor = {W.~McCune}, booktitle = {Proceedings of the 14th International Conference on Automated Deduction (Townsville, Australia)}, year = 1997, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer-Verlag}, volume = 1249, pages = {19--33}, url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/BaaTin-CADE-97.pdf}, } @TECHREPORT{BaaTin-RR-96, author = {Franz Baader and Cesare Tinelli}, title = {A New Approach for Combining Decision Procedures for the Word Problem, and Its Connection to the {N}elson-{O}ppen Combination Method}, institution = {LuFG Theoretical Computer Science, RWTH-Aachen, Germany}, year = 1996, number = {96-01}, } @INPROCEEDINGS{TinHar-CP-96, author = {Cesare Tinelli and Mehdi T.~Harandi}, title = {Constraint Logic Programming over Unions of Constraint Theories}, editor = {E.~C.~Freuder}, booktitle = {Proceedings of the 2nd International Conference on Principles and Practice of Constraint Programming, (Cambridge, MA, USA)}, month = aug, year = 1996, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {1118}, pages = {436--450}, url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/TinHar-CP-96.pdf}, } @INPROCEEDINGS{TinHar-FROCOS-96, author = {Cesare Tinelli and Mehdi T.~Harandi}, title = {A new correctness proof of the {N}elson--{O}ppen combination procedure}, editor = {F.~Baader and K.~U.~Schulz}, booktitle = {Frontiers of Combining Systems: Proceedings of the 1st International Workshop (Munich, Germany)}, publisher = {Kluwer Academic Publishers}, series = {Applied Logic}, month = mar, year = 1996, pages = {103--120}, url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/TinHar-FROCOS-96.pdf}, } @MASTERSTHESIS{Tin-MS-95, author = {Cesare Tinelli}, title = {Extending the {CLP} Scheme to Unions of Constraint Theories}, school = {Department of Computer Science, University of Illinois at Urbana-Champaign}, month = oct, year = 1995, address = {Urbana-Champaign, Illinois}, url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/Tin-MS-95.pdf}, }