A Generalized Factorization Rule Based on the Introduction of Skolem Terms. - Uwe Egly (ÖGAI, 1991)

A Simple Proof for the Pigeonhole Formulae. - Uwe Egly (ECAI, 1992)

Shortening Proofs by Quantifier Introduction. - Uwe Egly (LPAR, 1992)

On Different Concepts of Function Introduction. - Uwe Egly (Kurt Gödel Colloquium, 1993)

A First Order Resolution Calculus with Symmetries. - Uwe Egly (LPAR, 1993)

On methods of function introduction and related concepts. - Uwe Egly (1994)

KoMeT. - Wolfgang Bibel; Stefan Brüning; Uwe Egly; Thomas Rath (CADE, 1994)

On the Value of Antiprenexing. - Uwe Egly (LPAR, 1994)

Super-Polynomial Speed-Ups in Proof Length by New Tautologies. - Uwe Egly (EPIA, 1995)

Issues in Theorem Proving Based on the Connection Method. - Wolfgang Bibel; Stefan Brüning; Uwe Egly; Daniel S. Korn; Thomas Rath (TABLEAUX, 1995)

On the Practical Value of Different Definitional Translations to Normal Form. - Uwe Egly; Thomas Rath (CADE, 1996)

On Different Structure-Preserving Translations to Normal Form. - Uwe Egly (J. Symb. Comput., 1996)

Some Pitfalls of LK-to-LJ Translations and How to Avoid Them. - Uwe Egly (CADE, 1997)

Non-elementary Speed-Ups in Default Reasoning. - Uwe Egly; Hans Tompits (ECSQARU-FAPR, 1997)

Structuring of Computer-Generated Proofs by Cut Introduction. - Uwe Egly; Karin Genther (Kurt Gödel Colloquium, 1997)

Is Non-Monotonic Reasoning Always Harder? - Uwe Egly; Hans Tompits (LPNMR, 1997)

Lean Induction Principles for Tableaux. - Matthias Baaz; Uwe Egly; Christian G. Fermüller (TABLEAUX, 1997)

Non-elementary Speed-ups in Proof Length by Different Variants of Classical Analytic Calculi. - Uwe Egly (TABLEAUX, 1997)

A Sequent Calculus for Intuitionistic Default Logic. - Uwe Egly; Hans Tompits (WLP, 1997)

On Definitional Transformations to Normal Form for Institionistic Logic. - Uwe Egly (Fundam. Informaticae, 1997)

Intuitionistic Proof Transformations and Their Application to Constructive Program Synthesis. - Uwe Egly; Stephan Schmitt (AISC, 1998)

Quantifers and the System KE: Some Surprising Results. - Uwe Egly (CSL, 1998)

JQuest: ein javabasiertes Designtool für elektronische Fragebogen im Internet. - Uwe Egly; Gernot Koller (Interaktion im Web, 1998)

On Proof Complexity of Circumscription. - Uwe Egly; Hans Tompits (TABLEAUX, 1998)

Intuitionistic Proof Transformations: Complexity and Applications. - Uwe Egly; Stephan Schmitt (Proof Search in Type-Theoretic Languages@CADE, 1998)

An Answer to an Open Problem of Urquhart. - Uwe Egly (Theor. Comput. Sci., 1998)

A Web-based Tutoring Tool for Calculating Default Logic Extensions. - Uwe Egly; Michael Fink 001; Axel Polleres; Hans Tompits (WebNet, 1999)

On Intuitionistic Proof Transformations, their Complexity, and Application to Constructive Program Synthesis. - Uwe Egly; Stephan Schmitt (Fundam. Informaticae, 1999)

Solving Advanced Reasoning Tasks Using Quantified Boolean Formulas. - Uwe Egly; Thomas Eiter; Hans Tompits; Stefan Woltran (AAAI/IAAI, 2000)

Some Strengths of Nonmonotonic Reasoning. - Uwe Egly; Hans Tompits (Intellectics and Computational Logic, 2000)

Properties of Embeddings from Int to S4. - Uwe Egly (TABLEAUX, 2000)

Experimental Evaluation of the Disjunctive Logic Programming Module of the System QUIP. - Uwe Egly; Thomas Eiter; Volker Klotz; Hans Tompits; Stefan Woltran (WLP, 2000)

Implementing Default Reasoning Using Quantified Boolean Formulae. - Uwe Egly; Thomas Eiter; Hans Tompits; Stefan Woltran (WLP, 2000)

QUIP - A Tool for Computing Nonmonotonic Reasoning Tasks - Uwe Egly; Thomas Eiter; Hans Tompits; Stefan Woltran (CoRR, 2000)

Practically Useful Variants of Definitional Translations to Normal Form. - Uwe Egly; Thomas Rath (Inf. Comput., 2000)

Normal Form Transformations. - Matthias Baaz; Uwe Egly; Alexander Leitsch (Handbook of Automated Reasoning, 2001)

Computing Stable Models with Quantified Boolean Formulas: Some Experimental Results. - Uwe Egly; Thomas Eiter; Volker Klotz; Hans Tompits; Stefan Woltran (Answer Set Programming, 2001)

Deriving Modular Programs from Short Proofs. - Uwe Egly; Stephan Schmitt (IJCAR, 2001)

On Different Intuitionistic Calculi and Embeddings from Int to S4. - Uwe Egly (Stud Logica, 2001)

Proof-complexity results for nonmonotonic reasoning. - Uwe Egly; Hans Tompits (ACM Trans. Comput. Log., 2001)

Embedding Lax Logic into Intuitionistic Logic. - Uwe Egly (CADE, 2002)

Comparing Different Prenexing Strategies for Quantified Boolean Formulas. - Uwe Egly; Martina Seidl; Hans Tompits; Stefan Woltran; Michael Zolda (SAT, 2003)

On Different Proof-Search Strategies for Orthologic. - Uwe Egly; Hans Tompits (Stud Logica, 2003)

On deciding subsumption problems. - Uwe Egly; Reinhard Pichler; Stefan Woltran (Ann. Math. Artif. Intell., 2005)

Reasoning in Argumentation Frameworks Using Quantified Boolean Formulas. - Uwe Egly; Stefan Woltran (COMMA, 2006)

A Solver for QBFs in Nonprenex Form. - Uwe Egly; Martina Seidl; Stefan Woltran (ECAI, 2006)

Phase Transition for Random Quantified XOR-Formulas. - Nadia Creignou; Hervé Daudé; Uwe Egly (J. Artif. Intell. Res., 2007)

ASPARTIX: Implementing Argumentation Frameworks Using Answer-Set Programming. - Uwe Egly; Sarah Alice Gaggl; Stefan Woltran (ICLP, 2008)

New Results on the Phase Transition for Random Quantified Boolean Formulas. - Nadia Creignou; Hervé Daudé; Uwe Egly; Raphaël Rossignol (SAT, 2008)

A knowledge-based videotheodolite measurement system for object representation/monitoring. - Alexander Reiterer; Uwe Egly; Thomas Eiter; Heribert Kahmen (Adv. Eng. Softw., 2008)

(1, 2)-QSAT: A Good Candidate for Understanding Phase Transitions Mechanisms. - Nadia Creignou; Hervé Daudé; Uwe Egly; Raphaël Rossignol (SAT, 2009)

A solver for QBFs in negation normal form. - Uwe Egly; Martina Seidl; Stefan Woltran (Constraints An Int. J., 2009)

The threshold for random (1,2)-QSAT - Nadia Creignou; Hervé Daudé; Uwe Egly; Raphaël Rossignol (CoRR, 2009)

Knowledge-Based Geo-risk Assessment for an Intelligent Measurement System. - Tanja Vicovac; Alexander Reiterer; Uwe Egly; Thomas Eiter; Dirk Rieke-Zapp (IFIP AI, 2010)

Answer-set programming encodings for argumentation frameworks. - Uwe Egly; Sarah Alice Gaggl; Stefan Woltran (Argument Comput., 2010)

A SAT Solver for Circuits Based on the Tableau Method. - Uwe Egly; Leopold Haller (Künstliche Intell., 2010)

Towards Semantics-Aware Merge Support in Optimistic Model Versioning. - Petra Brosch; Uwe Egly; Sebastian Gabmeyer; Gerti Kappel; Martina Seidl; Hans Tompits; Magdalena Widl; Manuel Wimmer (MoDELS (Workshops), 2011)

Complexity of logic-based argumentation in Schaefer's framework. - Nadia Creignou; Uwe Egly; Johannes Schmidt 001 (COMMA, 2012)

On Sequent Systems and Resolution for QBFs. - Uwe Egly (SAT, 2012)

Guided Merging of Sequence Diagrams. - Magdalena Widl; Armin Biere; Petra Brosch; Uwe Egly; Marijn Heule; Gerti Kappel; Martina Seidl; Hans Tompits (SLE, 2012)

Towards Scenario-Based Testing of UML Diagrams. - Petra Brosch; Uwe Egly; Sebastian Gabmeyer; Gerti Kappel; Martina Seidl; Hans Tompits; Magdalena Widl; Manuel Wimmer (TAP@TOOLS, 2012)

A Framework for the Specification of Random SAT and QSAT Formulas. - Nadia Creignou; Uwe Egly; Martina Seidl (TAP@TOOLS, 2012)

Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving. - Uwe Egly; Florian Lonsing; Magdalena Widl (LPAR, 2013)

Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation. - Florian Lonsing; Uwe Egly; Allen Van Gelder (SAT, 2013)

Incremental QBF Solving. - Florian Lonsing; Uwe Egly (CP, 2014)

SAT-based methods for circuit synthesis. - Roderick Bloem; Uwe Egly; Patrick Klampfl; Robert Könighofer; Florian Lonsing (FMCAD, 2014)

Incremental QBF Solving by DepQBF. - Florian Lonsing; Uwe Egly (ICMS, 2014)

Complexity Classifications for Logic-Based Argumentation. - Nadia Creignou; Uwe Egly; Johannes Schmidt 001 (ACM Trans. Comput. Log., 2014)

Automated Benchmarking of Incremental SAT and QBF Solvers. - Uwe Egly; Florian Lonsing; Johannes Oetsch (LPAR, 2015)

Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination. - Florian Lonsing; Fahiem Bacchus; Armin Biere; Uwe Egly; Martina Seidl (LPAR, 2015)

Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API. - Florian Lonsing; Uwe Egly (SAT, 2015)

Exact location of the phase transition for random (1, 2)-QSAT. - Nadia Creignou; Hervé Daudé; Uwe Egly; Raphaël Rossignol (RAIRO Theor. Informatics Appl., 2015)

On Stronger Calculi for QBFs. - Uwe Egly (SAT, 2016)

Q-Resolution with Generalized Axioms. - Florian Lonsing; Uwe Egly; Martina Seidl (SAT, 2016)

Satisfiability-Based Methods for Reactive Synthesis from Safety Specifications. - Roderick Bloem; Uwe Egly; Patrick Klampfl; Robert Könighofer; Florian Lonsing; Martina Seidl (CoRR, 2016)

SAT and Interactions (Dagstuhl Seminar 16381). - Olaf Beyersdorff; Nadia Creignou; Uwe Egly; Heribert Vollmer (Dagstuhl Reports, 2016)

DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL. - Florian Lonsing; Uwe Egly (CADE, 2017)

Conformant planning as a case study of incremental QBF solving. - Uwe Egly; Martin Kronegger; Florian Lonsing; Andreas Pfandler (Ann. Math. Artif. Intell., 2017)

QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property. - Florian Lonsing; Uwe Egly (IJCAR, 2018)

Evaluating QBF Solvers: Quantifier Alternations Matter. - Florian Lonsing; Uwe Egly (CP, 2018)

Expansion-Based QBF Solving Without Recursion. - Roderick Bloem; Nicolas Braud-Santoni; Vedad Hadzic; Uwe Egly; Florian Lonsing; Martina Seidl (FMCAD, 2018)

QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties. - Florian Lonsing; Uwe Egly (SAT, 2019)

SAT and Interactions (Dagstuhl Seminar 20061). - Olaf Beyersdorff; Uwe Egly; Meena Mahajan; Cláudia Nalon (Dagstuhl Reports, 2020)

Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations. - Roderick Bloem; Nicolas Braud-Santoni; Vedad Hadzic; Uwe Egly; Florian Lonsing; Martina Seidl (Formal Methods Syst. Des., 2021)

Implementations for Shor's algorithm for the DLP. - Alexander Mandl; Uwe Egly (GI-Jahrestagung, 2022)