Uwe Egly
Ao.Univ.Prof. Dipl.-Ing. Dr.rer.nat.
Research Focus
- Logic and Computation: 100%
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
-
Associate Professor
Knowledge-Based Systems, E192-03
Courses
2024W
- Abstract Argumentation / 184.682 / VU
- Artificial Intelligence Seminar / 184.068 / SE
- Bachelor Thesis for Computer Science and Business Informatics / 184.713 / PR
- Formal Methods in Computer Science / 185.A93 / UE
- Formal Methods in Computer Science / 185.291 / VU
- Introduction to Knowledge-based Systems / 192.023 / VU
- Introduction to Quantum Computing, Complexity Theory, and Algorithmics / 192.042 / VU
- Project in Computer Science 1 / 192.021 / PR
- Project in Computer Science 2 / 192.022 / PR
- Quantum Computing / 192.070 / VU
- Quantum Computing, Complexity Theory, and Algorithmics / 192.043 / VU
- Scientific Research and Writing / 193.052 / SE
- Seminar for PhD Students / 184.721 / SE
- Seminar in Knowledge Representation and Reasoning / 184.712 / SE
- Seminar in Logic / 184.264 / SE
- Seminar in Theoretical Computer Science / 184.067 / SE
2025S
- Project in Computer Science 1 / 192.021 / PR
- Project in Computer Science 2 / 192.022 / PR
Projects
-
Quantified Boolean Formulas
2011 – 2019 / Austrian Science Fund (FWF)
Publications: 149733 / 149734 / 149737 / 151629 / 151824 / 157864 / 157902 / 23937 / 24255 / 39349 / 53735 / 53833 / 54131 / 54255 / 54407 / 54460 / 54461 / 54582 / 54587 / 54717 / 54893 / 54894 / 55227 / 55291 / 55294 / 55295 / 55296 / 55351 / 55748 / 55974 / 55980 / 56243 / 56244 / 56245 / 56821 / 56822 / 56844 / 57142 / 85468 / 85469 / 85891 / 85946 / 85997 / 85998 / 85999 / 86000 / 86001 / 86173 / 86432 / 86433 / 86434 / 86444 / 86672 / 86673 / 86674 -
FAME: Formalizing and Managing Evolution in Model-Driven Engineering
2011 – 2014 / Vienna Science and Technology Fund (WWTF)
Publications: 157902 / 53735 / 53833 / 54407 / 54893 / 54894 / 55748 / 55974 / 55980 -
QUIP--A computational framework for advanced reasoning tasks
2001 – 2004 / Austrian Science Fund (FWF)
Publications
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
- Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations / Bloem, R., Braud-Santoni, N., Hadzic, V., Egly, U., Lonsing, F., & Seidl, M. (2021). Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations. Formal Methods in System Design, 57(2), 157–177. https://doi.org/10.1007/s10703-021-00371-7
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
-
Conformant planning as a case study of incremental QBF solving
/
Egly, U., Kronegger, M., Lonsing, F., & Pfandler, A. (2017). Conformant planning as a case study of incremental QBF solving. Annals of Mathematics and Artificial Intelligence, 80(1), 21–45. http://hdl.handle.net/20.500.12708/147186
Projects: FAIR (2013–2018) / START (2014–2022) -
DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL
/
Lonsing, F., & Egly, U. (2017). DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL. In Automated Deduction – CADE 26 (pp. 371–384). Springer. https://doi.org/10.1007/978-3-319-63046-5_23
Project: Boolean (2011–2019) -
Evaluating QBF Solvers: Quantifier Alternations Matter
/
Lonsing, F., & Egly, U. (2017). Evaluating QBF Solvers: Quantifier Alternations Matter. http://hdl.handle.net/20.500.12708/39349
Project: Boolean (2011–2019)
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
-
Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
/
Lonsing, F., & Egly, U. (2015). Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API. In Theory and Applications of Satisfiability Testing -- SAT 2015 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings (pp. 191–198). Springer. https://doi.org/10.1007/978-3-319-24318-4_14
Project: Boolean (2011–2019) -
Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination
/
Lonsing, F., Bacchus, F., Biere, A., Egly, U., & Seidl, M. (2015). Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination. In Logic for Programming, Artificial Intelligence, and Reasoning (pp. 418–433). Springer. https://doi.org/10.1007/978-3-662-48899-7_29
Project: Boolean (2011–2019) -
Exact location of the phase transition for random (1,2)-QSAT
/
Creignou, N., Daudé, H., Egly, U., & Rossignol, R. (2015). Exact location of the phase transition for random (1,2)-QSAT. RAIRO - Theoretical Informatics and Applications, 49(1), 23–45. https://doi.org/10.1051/ita/2014025
Project: Boolean (2011–2019) -
Automated Benchmarking of Incremental SAT and QBF Solvers
/
Egly, U., Lonsing, F., & Oetsch, J. (2015). Automated Benchmarking of Incremental SAT and QBF Solvers. In Logic for Programming, Artificial Intelligence, and Reasoning (pp. 178–186). Springer. https://doi.org/10.1007/978-3-662-48899-7_13
Project: Boolean (2011–2019)
2014
-
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) -
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) -
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
- Complexity Classifications for logic-based Argumentation / Egly, U., Creignou, N., & Schmidt, J. (2013). Complexity Classifications for logic-based Argumentation. arXiv. https://doi.org/10.48550/arXiv.1304.5388
-
Guided Merging of Sequence Diagrams
/
Widl, M., Biere, A., Kaufmann, P., Egly, U., Heule, M., Kappel, G., Seidl, M., & Tompits, H. (2013). Guided Merging of Sequence Diagrams. In Software Language Engineering (pp. 164–183). Lecture Notes in Computer Science Volume 7745. https://doi.org/10.1007/978-3-642-36089-3_10
Projects: Boolean (2011–2019) / FAME (2011–2014) -
Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving
/
Egly, U., Lonsing, F., & Widl, M. (2013). Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving. In K. McMillan, A. Middeldorp, & A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning (pp. 291–308). Springer. https://doi.org/10.1007/978-3-642-45221-5_21
Projects: Boolean (2011–2019) / FAME (2011–2014) - Questions around quantified boolean formulas / Egly, U. (2013). Questions around quantified boolean formulas. ANR Boole Réunion Finale, Paris, Frankreich, EU. http://hdl.handle.net/20.500.12708/85685
- Solving quantified Boolean formula / Egly, U. (2013). Solving quantified Boolean formula. Journées ANR BOOLE, Marseille, Frankreich, EU. http://hdl.handle.net/20.500.12708/85684
- Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation / Lonsing, F., Egly, U., & Van Gelder, A. (2013). Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation. In Theory and Applications of Satisfiability Testing – SAT 2013 (pp. 100–115). https://doi.org/10.1007/978-3-642-39071-5_9
-
Solution extraction from long-distance resolution proofs
/
Egly, U., & Widl, M. (2013). Solution extraction from long-distance resolution proofs. In M. Seidl & F. Lonsing (Eds.), International Workshop on Quantified Boolean Formulas 2013 Informal Workshop Report (p. 10). http://hdl.handle.net/20.500.12708/54894
Projects: Boolean (2011–2019) / FAME (2011–2014)
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
- DPLL Procedures for Non-clausal SAT and QSAT Problems / Egly, U. (2011). DPLL Procedures for Non-clausal SAT and QSAT Problems. Workshop on Computational Logics and Applications, Wien, Austria. http://hdl.handle.net/20.500.12708/85220
-
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. (2011). Towards Semantics-Aware Merge Support in Optimistic Model Versioning. In Proceedings of the Models and Evolution Workshop @ MoDELS’11 (p. 10). http://hdl.handle.net/20.500.12708/53735
Projects: Boolean (2011–2019) / FAME (2011–2014) / FAME (2011–2014)
2010
-
Answer-Set Programming Encodings for Argumentation Frameworks
/
Egly, U., Gaggl, S., & Woltran, S. (2010). Answer-Set Programming Encodings for Argumentation Frameworks. Argument and Computation, 1(2), 147–177. http://hdl.handle.net/20.500.12708/167366
Projects: Argu (2009–2012) / TTPC (2008–2012) - Application of artificial intelligence in Geodesy - A review of theoretical foundations and practical examples / Reiterer, A., Egly, U., Vicovac, T., Mai, E., Moafipoor, S., Grejner-Brzezinska, D. A., & Toth, C. K. (2010). Application of artificial intelligence in Geodesy - A review of theoretical foundations and practical examples. Journal of Applied Geodesy, 4(4). https://doi.org/10.1515/jag.2010.020
- A SAT Solver for Circuits Based on the Tableau Method / Egly, U., & Haller, L. (2010). A SAT Solver for Circuits Based on the Tableau Method. KI - Künstliche Intelligenz, 24(1), 15–23. https://doi.org/10.1007/s13218-010-0008-4
- Intelligent Deformation Interpretation / Vicovac, T., Reiterer, A., Egly, U., Eiter, T., & Rieke-Zapp, D. (2010). Intelligent Deformation Interpretation. In A. Reiterer, U. Egly, M. Heinert, & B. Riedel (Eds.), Application of Artificial Intelligence and Innovations in Engineering Geodesy (AIEG 2010) (pp. 10–20). http://hdl.handle.net/20.500.12708/42560
- Knowledge-Based Geo-risk Assessment for an Intelligent Measurement System / Vicovac, T., Reiterer, A., Egly, U., Eiter, T., & Rieke-Zapp, D. (2010). Knowledge-Based Geo-risk Assessment for an Intelligent Measurement System. In M. Bramer (Ed.), Artificial Intelligence in Theory and Practice III (pp. 215–224). Springer. https://doi.org/10.1007/978-3-642-15286-3_21
2009
- (1,2)-QSAT: A Good Candidate for Understanding Phase Transitions Mechanisms / Creignou, N., Daudé, H., Egly, U., & Rossignol, R. (2009). (1,2)-QSAT: A Good Candidate for Understanding Phase Transitions Mechanisms. In O. Kullmann (Ed.), Theory and Applications of Satisfiability Testing - SAT 2009 (pp. 363–376). Springer Lecture Notes in Computer Science (LNCS). https://doi.org/10.1007/978-3-642-02777-2_34
- A Solver for QBFs in Negation Normal Form / Egly, U., Seidl, M., & Woltran, S. (2009). A Solver for QBFs in Negation Normal Form. Constraints, 14(1), 38–79. http://hdl.handle.net/20.500.12708/165275
- A 3D optical deformation measurement system supported by knowledge-based and learning techniques / Reiterer, A., Lehmann, M., Miljanovic, M., Ali, H., Paar, G., Egly, U., Eiter, T., & Kahmen, H. (2009). A 3D optical deformation measurement system supported by knowledge-based and learning techniques. Journal of Applied Geodesy, 3(1), 1–13. http://hdl.handle.net/20.500.12708/165576
- First Developement steps for an Automated Knowledge-Based Deformation Interpretation System / Vicovac, T., Reiterer, A., Egly, U., Eiter, T., & Rieke-Zapp, D. (2009). First Developement steps for an Automated Knowledge-Based Deformation Interpretation System. In A. Grün & H. Kahmen (Eds.), Optical 3-D Measurement Techniques IX (pp. 61–90). http://hdl.handle.net/20.500.12708/42385
2008
- A knowledge-based videotheodolite measurement system for object representation /monitoring / Reiterer, A., Egly, U., Eiter, T., & Kahmen, H. (2008). A knowledge-based videotheodolite measurement system for object representation /monitoring. Advances in Engineering Software, 39(10), 821–827. http://hdl.handle.net/20.500.12708/168962
- Answer-Set Programming Encodings for Argumentation Frameworks / Egly, U., Gaggl, S. A., & Woltran, S. (2008). Answer-Set Programming Encodings for Argumentation Frameworks. In W. Faber & J. Lee (Eds.), ICLP-Workshop Proceedings; Proceedings of the 1st International Workshop on Answer Set Programming and Other Computing Paradigms, ASPOCP 2008 (pp. 1–15). http://hdl.handle.net/20.500.12708/52469
- Deformation Monitoring by Image Assisted Total Stations - State of the Art and Future Developments / Reiterer, A., Bauer, A., & Egly, U. (2008). Deformation Monitoring by Image Assisted Total Stations - State of the Art and Future Developments. Technologieforum Leica Geosystems, Heerbrugg, Schweiz, Non-EU. http://hdl.handle.net/20.500.12708/82156
- New Results on the Phase Transition for Random Quantified Boolean Formulas / Creignou, N., Daude, H., Egly, U., & Rossignol, R. (2008). New Results on the Phase Transition for Random Quantified Boolean Formulas. In Theory and Application of Satisfiability Testing --- SAT 2008 (pp. 34–47). Lecture Notes in Computer Science. http://hdl.handle.net/20.500.12708/52643
- ASPARTIX: Implementing Argumentation Frameworks Using Answer-Set Programming / Egly, U., Gaggl, S. A., & Woltran, S. (2008). ASPARTIX: Implementing Argumentation Frameworks Using Answer-Set Programming. In M. G. de la Banda & E. Pontelli (Eds.), Proceedings of the 24#^{th} Conference on Logic Programming (ICLP’08) (pp. 734–738). Springer. http://hdl.handle.net/20.500.12708/52465
- Case-Based Deformation Assessment - A Concept / Lehmann, M., & Reiterer, A. (2008). Case-Based Deformation Assessment - A Concept. In A. Reiterer & U. Egly (Eds.), Application of Artificial Intelligence in Engineering Geodesy (pp. 91–98). http://hdl.handle.net/20.500.12708/42283
- Ein bildgestütztes 3D Deformationsmesssystem (An Image-Based 3D Deformation Measurement System) / Reiterer, A., Lehmann, M., Miljanovic, M., Ali, H., Paar, G., Egly, U., Eiter, T., & Kahmen, H. (2008). Ein bildgestütztes 3D Deformationsmesssystem (An Image-Based 3D Deformation Measurement System). In Journal of Alpine Geology, Pangeo 2008 (p. 87). Mitt. Ges. Geol. Bergbaustud. Österr. http://hdl.handle.net/20.500.12708/42265
- Deformation Monitoring using a new kind of Optical 3D Measurement System: Components and Perspectives / Reiterer, A., Lehmann, M., Miljanovic, M., Ali, H., Paar, G., Egly, U., Eiter, T., & Kahmen, H. (2008). Deformation Monitoring using a new kind of Optical 3D Measurement System: Components and Perspectives. In Measuring the Change (p. 10). http://hdl.handle.net/20.500.12708/42215
- A Solver for QBFs in Negation Normal Form / Egly, U., Seidl, M., & Woltran, S. (2008). A Solver for QBFs in Negation Normal Form (INFSYS RR-1843-08-03). http://hdl.handle.net/20.500.12708/35354
- Answer-Set Programming Encodings for Argumentation Frameworks / Egly, U., Gaggl, S. A., & Woltran, S. (2008). Answer-Set Programming Encodings for Argumentation Frameworks (DBAI-TR-2008-62). http://hdl.handle.net/20.500.12708/35164
- Application of Artificial Intelligence in Engineering Geodesy / Reiterer, A., & Egly, U. (Eds.). (2008). Application of Artificial Intelligence in Engineering Geodesy. Eigenverlag. http://hdl.handle.net/20.500.12708/22790
2007
- Phase Transition for Random Quantified XOR-Formulas / Creignou, N., Daude, H., & Egly, U. (2007). Phase Transition for Random Quantified XOR-Formulas. Journal of Artificial Intelligence Research, 29, 1–18. http://hdl.handle.net/20.500.12708/169673
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
- On Deciding Subsumption Problems / Egly, U., Pichler, R., & Woltran, S. (2003). On Deciding Subsumption Problems. http://hdl.handle.net/20.500.12708/32928
- Beyond DP: Alternative Calculi for QBF Solving / Egly, U. (2003). Beyond DP: Alternative Calculi for QBF Solving. QBF-symposium, Paris, France, Austria. http://hdl.handle.net/20.500.12708/84235
Supervisions
2023
-
Design and implementation of the recursive Bernstein-Vazirani quantum algorithm
/
Zachmann, R. (2023). Design and implementation of the recursive Bernstein-Vazirani quantum algorithm [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2023.99331
Download: PDF (826 KB)
2021
-
Quantum algorithms for the discrete logarithm problem
/
Mandl, A. (2021). Quantum algorithms for the discrete logarithm problem [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2021.89440
Download: PDF (908 KB) -
Sequent Calculi for QBFs : Their relation to bounded arithmetic, and the complexity of the witnessing problem
/
Jomar, D. (2021). Sequent Calculi for QBFs : Their relation to bounded arithmetic, and the complexity of the witnessing problem [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2021.75860
Download: PDF (840 KB)
2019
-
Realising argumentation using answer set programming and quantified boolean formulas
/
Diller, M. (2019). Realising argumentation using answer set programming and quantified boolean formulas [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2019.66428
Download: PDF (1.53 MB)
2016
-
Symbolic methods for the verification of software models
/
Widl, M. (2016). Symbolic methods for the verification of software models [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2016.36020
Download: PDF (1.3 MB)
2015
-
Deformation monitoring using artificial intelligence techniques
/
Miljanović, M. (2015). Deformation monitoring using artificial intelligence techniques [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2015.24501
Download: PDF (12.2 MB)
2013
-
A comprehensive analysis of the cf2 argumentation semantics : from characterization to implementation
/
Gaggl, S. A. (2013). A comprehensive analysis of the cf2 argumentation semantics : from characterization to implementation [Dissertation, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-54957
Download: PDF (4.13 MB)
2011
- QPar : a multithreaded distributed solver for quantified Boolean formulas / Matzke, T. (2011). QPar : a multithreaded distributed solver for quantified Boolean formulas [Diploma Thesis, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/160501
-
GQBF and proof complexity
/
Haberl, P. (2011). GQBF and proof complexity [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-43748
Download: PDF (684 KB) -
EM4J - an explanation module toolbox for Jess
/
Wurzer, S. (2011). EM4J - an explanation module toolbox for Jess [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-60540
Download: PDF (2.14 MB) - Workspace decomposition-based motion planning / Kogelnig, R. (2011). Workspace decomposition-based motion planning [Diploma Thesis, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/160476
2010
- Preprocessing for quantified Boolean formulas / Petzelbauer, M. (2010). Preprocessing for quantified Boolean formulas [Diploma Thesis, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/161371
2009
- Solving argumentation frameworks using answer set programming / Gaggl, S. A. (2009). Solving argumentation frameworks using answer set programming [Diploma Thesis, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/185659
2008
-
Anforderungen, Konzeption und Schnittstellen für ein medizinisches Multimediaarchiv
/
Leder, S. (2008). Anforderungen, Konzeption und Schnittstellen für ein medizinisches Multimediaarchiv [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-22312
Download: PDF (592 KB) - Extending a tableau-based SAT procedure with techniques from CNF-based SAT / Haller, L. C. R. (2008). Extending a tableau-based SAT procedure with techniques from CNF-based SAT [Diploma Thesis, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/182091
2007
-
A solver for quantified boolean formulas in negation normal form
/
Seidl, M. (2007). A solver for quantified boolean formulas in negation normal form [Dissertation, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-21782
Download: PDF (748 KB) -
New upper bounds for the SAT/UNSAT threshold for shapes
/
Santillán Rodríguez, R. (2007). New upper bounds for the SAT/UNSAT threshold for shapes [Master Thesis, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-21135
Download: PDF (488 KB) -
Three-dimensional drawing of lattice-like structures
/
Ziegler, G. (2007). Three-dimensional drawing of lattice-like structures [Master Thesis, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-17549
Download: PDF (1.82 MB) -
Investigations on intuitionistic logic and modal logic
/
Seidelmann, P. (2007). Investigations on intuitionistic logic and modal logic [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-17714
Download: PDF (444 KB) -
Ein interaktives E-Learning System für die Grundlagen der mathematischen Logik
/
Eibegger, M. (2007). Ein interaktives E-Learning System für die Grundlagen der mathematischen Logik [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-16173
Download: PDF (4.32 MB)
2006
-
Counter lattice generation for non-provable formulas
/
Zugaj, A. (2006). Counter lattice generation for non-provable formulas [Master Thesis, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-37126
Download: PDF (335 KB)
2005
- Decision making in the robot soccer domain / Weber, D. (2005). Decision making in the robot soccer domain [Diploma Thesis, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/184612
- Collisions in cryptographic hash algorithms / Neumeier, E. (2005). Collisions in cryptographic hash algorithms [Diploma Thesis, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/184494
2004
-
Comparing different prenexing strategies for quantified boolean formulas
/
Zolda, M. (2004). Comparing different prenexing strategies for quantified boolean formulas [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-9643
Download: PDF (1.33 MB) -
Real-time monitoring for the time-triggered architecture
/
Smaili, I. (2004). Real-time monitoring for the time-triggered architecture [Dissertation, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-12690
Download: PDF (8.47 MB) - Nano - Entwicklung eines kleinen sechsbeinigen Roboters nach biologischem Vorbild / Tappeiner, H. W. (2004). Nano - Entwicklung eines kleinen sechsbeinigen Roboters nach biologischem Vorbild [Diploma Thesis, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/184109
2003
- Das Enigma System : Aufbau und Kryptoanalyse / Mayr, T. (2003). Das Enigma System : Aufbau und Kryptoanalyse [Diploma Thesis, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/183655
- Inhaltsausgezeichnete Erstellung und Publikation technischer Dokumentation / Schiemann, B. (2003). Inhaltsausgezeichnete Erstellung und Publikation technischer Dokumentation [Diploma Thesis, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/183649
- Quantified Boolean formulas - from theory to practice / Woltran, S. (2003). Quantified Boolean formulas - from theory to practice [Dissertation, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/183034
2001
- The system QUIP: a solver for advanced reasoning tasks using quantified boolean formulas / Klotz, V. (2001). The system QUIP: a solver for advanced reasoning tasks using quantified boolean formulas [Diploma Thesis, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/180017
- iKE - ein intuitionistischer Kalkül / Marczy, W. (2001). iKE - ein intuitionistischer Kalkül [Diploma Thesis, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/180014