TU Wien Informatics

20 Years

Uwe Egly

Ao.Univ.Prof. Dipl.-Ing. Dr.rer.nat.

Research Focus

Research Areas

  • Automated Reasoning, Knowledge Reprensentation and Reasoning

About

Research interests: proof theory and proof complexity, knowledge representation and reasoning, computational logic, satisfiability checking for QBFs (Quantified Boolean Formulas), argumentation and argumentation frameworks, algorithms for pathplanning and applications of AI methods in engineering.

Role

2022

  • Implementations for Shor's algorithm for the DLP / Mandl, A., & Egly, U. (2022). Implementations for Shor’s algorithm for the DLP. In 52. Jahrestagung der Gesellschaft für Informatik (pp. 1133–1143). Gesellschaft für Informatik. https://doi.org/10.18420/inf2022_96

2021

2020

  • SAT and Interactions (Dagstuhl Seminar 20061) / Beyersdorff, O., Egly, U., Mahajan, M., & Nalon, C. (Eds.). (2020). SAT and Interactions (Dagstuhl Seminar 20061). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany. https://doi.org/10.4230/DagRep.10.2.1

2019

  • QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties / Lonsing, F., & Egly, U. (2019). QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties. In Theory and Applications of Satisfiability Testing – SAT 2019 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9–12, 2019, Proceedings (pp. 203–210). LNCS. https://doi.org/10.1007/978-3-030-24258-9_14

2018

  • Evaluating QBF Solvers: Quantifier Alternations Matter / Lonsing, F., & Egly, U. (2018). Evaluating QBF Solvers: Quantifier Alternations Matter. In Principles and Practice of Constraint Programming 24th International Conference, CP 2018, Lille, France, August 27-31, 2018, Proceedings (pp. 276–294). Springer. https://doi.org/10.1007/978-3-319-98334-9_19
  • Expansion-Based QBF Solving Without Recursion / Bloem, R., Braud-Santoni, N., Hadzic, V., Egly, U., Lonsing, F., & Seidl, M. (2018). Expansion-Based QBF Solving Without Recursion. In 2018 Formal Methods in Computer Aided Design (FMCAD). International Conference on Formal Methods in Computer-Aided Design (FMCAD), Portland, OR, USA, Non-EU. IEEE. https://doi.org/10.23919/fmcad.2018.8603004
  • $${\textsf {QRAT}}^{+}$$: Generalizing QRAT by a More Powerful QBF Redundancy Property / Lonsing, F., & Egly, U. (2018). $${\textsf {QRAT}}^{+}$$: Generalizing QRAT by a More Powerful QBF Redundancy Property. In Automated Reasoning (pp. 161–177). LNCS. https://doi.org/10.1007/978-3-319-94205-6_12

2017

2016

  • Q-Resolution with Generalized Axioms / Lonsing, F., Egly, U., & Seidl, M. (2016). Q-Resolution with Generalized Axioms. In Theory and Applications of Satisfiability Testing – SAT 2016 (pp. 435–452). Springer. https://doi.org/10.1007/978-3-319-40970-2_27
    Project: Boolean (2011–2019)
  • Conformant Planning as a Case Study of Incremental QBF Solving / Egly, U., Kronegger, M., Lonsing, F., & Pfandler, A. (2016). Conformant Planning as a Case Study of Incremental QBF Solving. Annals of Mathematics and Artificial Intelligence, 80(1), 21–45. https://doi.org/10.1007/s10472-016-9501-2
    Project: Boolean (2011–2019)
  • Translations from QBFs to First-order Logic / Egly, U. (2016). Translations from QBFs to First-order Logic. Deduktionstreffen, Klagenfurt, Austria. http://hdl.handle.net/20.500.12708/86444
    Project: Boolean (2011–2019)
  • On Stronger Calculi for QBFs / Egly, U. (2016). On Stronger Calculi for QBFs. In Theory and Applications of Satisfiability Testing – SAT 2016 (pp. 419–434). Springer. https://doi.org/10.1007/978-3-319-40970-2_26
    Project: Boolean (2011–2019)

2015

2014

  • Complexity Classifications for Logic-Based Argumentation / Creignou, N., Egly, U., & Schmidt, J. (2014). Complexity Classifications for Logic-Based Argumentation. ACM Transactions on Computational Logic, 15(3), 1–20. https://doi.org/10.1145/2629421
    Project: Boolean (2011–2019)
  • QBF Resolution Systems and Their Proof Complexities / Balabanov, V., Widl, M., & Jiang, J.-H. R. (2014). QBF Resolution Systems and Their Proof Complexities. In C. Sinz & U. Egly (Eds.), Theory and Applications of Satisfiability Testing - SAT 2014 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings (pp. 154–169). LNCS / Springer. https://doi.org/10.1007/978-3-319-09284-3_12
    Projects: Boolean (2011–2019) / FAME (2011–2014)
  • Incremental QBF Solving / Lonsing, F., & Egly, U. (2014). Incremental QBF Solving. In Principles and Practice of Constraint Programming 20th International Conference, CP 2014, Lyon, France, September 8-12, 2014, Proceedings (pp. 514–530). Springer. https://doi.org/10.1007/978-3-319-10428-7_38
    Project: Boolean (2011–2019)
  • Conformant Planning as a Case Study of Incremental QBF Solving / Egly, U., Kronegger, M., Lonsing, F., & Pfandler, A. (2014). Conformant Planning as a Case Study of Incremental QBF Solving. In Artificial Intelligence and Symbolic Computation (pp. 120–131). Springer. https://doi.org/10.1007/978-3-319-13770-4_11
    Projects: Boolean (2011–2019) / FAIR (2013–2018)
  • Deduction Concepts for Quantified Boolean Formulas / Egly, U. (2014). Deduction Concepts for Quantified Boolean Formulas. Advanced Winter School on Reasoning Engines for Rigorous System Engineering, Johannes Kepler University, Linz, Austria. http://hdl.handle.net/20.500.12708/86000
    Project: Boolean (2011–2019)
  • Quantifier Handling in Different Calculi for Quantified Boolean Formulas / Egly, U. (2014). Quantifier Handling in Different Calculi for Quantified Boolean Formulas. Algebra, Logic and Algorithms seminar, University of Leeds, United Kingdom, EU. http://hdl.handle.net/20.500.12708/85999
    Project: Boolean (2011–2019)
  • On the Relation between Resolution Calculi for QBFs and First-order Formulas / Egly, U. (2014). On the Relation between Resolution Calculi for QBFs and First-order Formulas. International Workshop on Quantified Boolean Formulas, Helsinki, EU. http://hdl.handle.net/20.500.12708/85998
    Project: Boolean (2011–2019)
  • Quantifier handling in calculi for quantified Boolean formulas / Egly, U. (2014). Quantifier handling in calculi for quantified Boolean formulas. International Workshop on Quantification (QUANTIFY), Wien, Austria. http://hdl.handle.net/20.500.12708/85997
    Project: Boolean (2011–2019)
  • Conformant Planning as a Case Study of Incremental QBF Solving / Egly, U., Kronegger, M., Lonsing, F., & Pfandler, A. (2014). Conformant Planning as a Case Study of Incremental QBF Solving. International Workshop on Quantified Boolean Formulas, Helsinki, EU. http://hdl.handle.net/20.500.12708/85946
    Projects: Boolean (2011–2019) / FAIR (2013–2018)
  • SAT-Based Methods for Circuit Synthesis / Bloem, R., Egly, U., Klampfl, P., Könighofer, R., & Lonsing, F. (2014). SAT-Based Methods for Circuit Synthesis. In Formal Methods in Computer-Aided Design (pp. 31–34). IEEE. http://hdl.handle.net/20.500.12708/55291
    Project: Boolean (2011–2019)
  • Incremental QBF Solving by DepQBF / Lonsing, F., & Egly, U. (2014). Incremental QBF Solving by DepQBF. In Mathematical Software – ICMS 2014 (pp. 307–314). Springer. https://doi.org/10.1007/978-3-662-44199-2_48
    Project: Boolean (2011–2019)
  • Theory and Applications of Satisfiability Testing – SAT 2014 / Theory and Applications of Satisfiability Testing – SAT 2014. (2014). In C. Sinz & U. Egly (Eds.), Lecture Notes in Computer Science. Springer. https://doi.org/10.1007/978-3-319-09284-3
    Project: Boolean (2011–2019)

2013

2012

  • Detection of Windows in Facades Using Image Processing Algorithms / Miljanovic, M., Egly, U., & Eiter, T. (2012). Detection of Windows in Facades Using Image Processing Algorithms. Indian Journal of Computer Science and Engineering, 3(4), 539–547. http://hdl.handle.net/20.500.12708/164414
  • Guided Merging of Sequence Diagrams / Widl, M., Biere, A., Kaufmann, P., Egly, U., Heule, M., Kappel, G., Seidl, M., & Tompits, H. (2012). Guided Merging of Sequence Diagrams. In K. Czarnecki & G. Hedin (Eds.), SLE 2012 - Pre-proceedings (pp. 163–182). http://hdl.handle.net/20.500.12708/54255
    Projects: Boolean (2011–2019) / FAME (2011–2014)
  • On sequent systems and resolution for quantified boolean formulas / Egly, U. (2012). On sequent systems and resolution for quantified boolean formulas. Dagstuhl Seminar 12471 - SAT Interactions, Dagstuhl, Deutschland, EU. http://hdl.handle.net/20.500.12708/85469
    Project: Boolean (2011–2019)
  • A new learning scheme for QDPLL solvers / Egly, U. (2012). A new learning scheme for QDPLL solvers. Dagstuhl Seminar 12461: Games and Decisions for Rigorous Systems Engineering, Dagstuhl, Deutschland, EU. http://hdl.handle.net/20.500.12708/85468
    Project: Boolean (2011–2019)
  • Complexity of logic-based argumentation in Schaefer's framework / Egly, U., Creignou, N., & Schmidt, J. (2012). Complexity of logic-based argumentation in Schaefer’s framework. In B. Verheij, S. Szeider, & S. Woltran (Eds.), Computational Models of Argument (pp. 237–248). IOS Press. http://hdl.handle.net/20.500.12708/54461
    Project: Boolean (2011–2019)
  • On Sequent Systems and Resolution for QBFs / Egly, U. (2012). On Sequent Systems and Resolution for QBFs. In Theory and Applications of Satisfiability Testing – SAT 2012 (pp. 100–113). Lecture Notes in Computer Science, Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-31612-8_9
    Project: Boolean (2011–2019)
  • Towards Semantics-Aware Merge Support in Optimistic Model Versioning / Kaufmann, P., Egly, U., Gabmeyer, S., Kappel, G., Seidl, M., Tompits, H., Widl, M., & Wimmer, M. (2012). Towards Semantics-Aware Merge Support in Optimistic Model Versioning. In Models in Software Engineering (pp. 246–256). Springer LNCS. https://doi.org/10.1007/978-3-642-29645-1_24
    Projects: Boolean (2011–2019) / FAME (2011–2014)
  • Towards Scenario-Based Testing of UML Diagrams / Kaufmann, P., Egly, U., Gabmeyer, S., Kappel, G., Seidl, M., Tompits, H., Widl, M., & Wimmer, M. (2012). Towards Scenario-Based Testing of UML Diagrams. In Tests and Proofs (pp. 149–155). Springer. https://doi.org/10.1007/978-3-642-30473-6_12
    Projects: Boolean (2011–2019) / FAME (2011–2014)
  • A Framework for the Specification of Random SAT and QSAT Formulas / Creignou, N., Egly, U., & Seidl, M. (2012). A Framework for the Specification of Random SAT and QSAT Formulas. In Proceedings of the 6th International Conference on Tests and Proofs (TAP 2012) (pp. 163–168). Springer. http://hdl.handle.net/20.500.12708/54164
    Project: FAME (2011–2014)

2011

2010

2009

2008

2007

2006

  • Phase Transition for Random Quantified XOR-formulas / Creignou, N., Daude, H., & Egly, U. (2006). Phase Transition for Random Quantified XOR-formulas. In Proceedings of the Guangzhou Symposioum on Satisfiability in Logic-Based Modeling (p. 12). http://hdl.handle.net/20.500.12708/51625
  • A Solver for QBFs in Nonprenex Form: Overview and Experimental Results / Egly, U., Seidl, M., & Woltran, S. (2006). A Solver for QBFs in Nonprenex Form: Overview and Experimental Results. In Proceedings of the Guangzhou Symposioum on Satisfiability in Logic-Based Modeling (p. 11). http://hdl.handle.net/20.500.12708/51624
    Project: ModelCVS (2006–2007)
  • Reasoning in Argumentation Frameworks Using Quantified Boolean Formulas / Egly, U., & Woltran, S. (2006). Reasoning in Argumentation Frameworks Using Quantified Boolean Formulas. In P. E. Dunne & T. J. M. Bench-Capon (Eds.), Proceedings of the 1st International Conference on Computational Models of Argument (COMMA 2006) (pp. 133–144). IOS Press. http://hdl.handle.net/20.500.12708/51590
  • A Solver for QBFs in Nonprenex Form / Egly, U., Seidl, M., & Woltran, S. (2006). A Solver for QBFs in Nonprenex Form. In Proceedings of the ECAI 2006 (pp. 477–481). IOS Press. http://hdl.handle.net/20.500.12708/51448
    Project: ModelCVS (2006–2007)

2005

  • On Deciding Subsumption Problems / Egly, U., Pichler, R., & Woltran, S. (2005). On Deciding Subsumption Problems. Annals of Mathematics and Artificial Intelligence, 43(1–4), 255–294. http://hdl.handle.net/20.500.12708/173345
  • Decision Making for MiroSOT Soccer Playing Robots / Egly, U., Novak, G., & Weber, D. (2005). Decision Making for MiroSOT Soccer Playing Robots. In Decision Making for MiroSOT Soccer Playing Robots (pp. 69–72). http://hdl.handle.net/20.500.12708/68833
  • A Smart Videometric System / Reiterer, A., Kahmen, H., Eiter, T., Egly, U., & Paar, G. (2005). A Smart Videometric System. In A. Grün & H. Kahmen (Eds.), Proceedings Optical 3-D Measurement Techniques VII, Vol. II (pp. 370–375). http://hdl.handle.net/20.500.12708/41914
  • A Knowledge-Based Decision System for an Image-Based Measurement / Reiterer, A., Egly, U., Eiter, T., & Kahmen, H. (2005). A Knowledge-Based Decision System for an Image-Based Measurement. In B. H. V. Topping (Ed.), Proceedings of the Eighth International Conference on the Application of Artificial Intelligence to Civil, Structural and Environmental Engineering (pp. 35–36). http://hdl.handle.net/20.500.12708/41891

2004

  • Argumentation Frameworks and QBFs / Egly, U. (2004). Argumentation Frameworks and QBFs. International Workshop on QSAT and SAT, Guangzhou, P.R. China, Austria. http://hdl.handle.net/20.500.12708/84320

2003

 

2023

2021

2019

2016

2015

2013

2011

2010

2009

2008

2007

2006

2005

2004

2003

2001