Database Entry Point
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-INF RG1 Publications , MPG Format, generated: Saturday, 1. November 2014

Scientific Publications for 2012

Blanchette, J.C., A. Popescu, D. Wand and C. Weidenbach: More SPASS with Isabelle : superposition with hard sorts and configurable simplification. In: Interactive Theorem Proving : Third Int. Conf., ITP 2012, Lect. Notes Comput. Sci. 7406, (Eds.) L. Beringer, A. Felty. Springer, Berlin 2012, 345-360.

Damm, W., H. Dierks, S. Disch, W. Hagemann, F. Pigorsch, C. Scholl, U. Waldmann and B. Wirtz: Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces. Science of Computer Programming 77, 1122-1150 (2012).

Fietzke, A., E. Kruglov and C. Weidenbach: Automatic generation of invariants for circular derivations in SUP(LA). In: Logic for Programming, Artificial Intelligence, and Reasoning : 18th Int. Conf., LPAR-18, Lect. Notes Comput. Sci. 7180, (Eds.) N. Bjørner, A. Voronkov. Springer, Berlin 2012, 197-211.

Fontaine, P., S. Merz and C. Weidenbach: Combination of disjoint theories: beyond decidability. In: Proc. 6th Int. Joint Conf. on Automated Reasoning, Lect. Notes Comput. Sci. 7364 [***Warning: Editor(s) might be missing!]. Springer, Berlin Heidelberg 2012, [***Warning: Pages missing!].

Kruglov, E. and C. Weidenbach: Superposition decides the first-order logic fragment over ground theories. Mathematics in Computer Science 6, 427-456 (2012).

Peltier, N. and V. Sofronie-Stokkermans: First-order theorem proving: foreword. Journal of Symbolic Computation 47, 1009-1010 (2012).

Suda, M. and C. Weidenbach: A PLTL-prover based on labelled superposition with partial model guidance. In: Automated Reasoning : 6th Int. Joint Conf., IJCAR 2012, Lect. Notes Comput. Sci. 7364, (Eds.) B. Gramlich, D. Miller, U. Sattler. Springer, Berlin 2012, 537-543.

- Labelled superposition for PLTL. In: Logic for Programming, Artificial Intelligence, and Reasoning : 18th Int. Conf., LPAR-18, Lect. Notes Comput. Sci. 7180, (Eds.) N. Bjørner, A. Voronkov. Springer, Berlin 2012, 391-405.

Publikationen im Internet

Fietzke, A. and C. Weidenbach: Superposition as a decision procedure for timed automata. Mathematics in Computer Science 6, 409-425 (2012). Internet: <http://link.springer.com/content/pdf/10.1007%2Fs11786-012-0134-5>

Weidenbach, C. and P. Wischnewski: Satisfiability checking and query answering for large ontologies. In: PAAR-2012 : Third Workshop on Practical Aspects of Automated Reasoning. PAAR-2012, Manchester 2012, 163-177 Internet: <http://www.eprover.org/EVENTS/PAAR-2012/PAAR2012.pdf>.

Bachelor Thesis

Bromberger, M.: Adapting the simplex algorithm for superposition modulo linear arithmetic. Universität des Saarlandes 2012.

Master's thesis

Azmy, N.: Formula renaming with generalizations. Universität des Saarlandes 2012.

Doctoral dissertation

Wischnewski, P.: Efficient reasoning procedures for complex first-order theories. Universität des Saarlandes 2012.