2025S

• Automated Deduction / 184.774 / VU

• VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic / Schoisswohl, J., Kovács, L., & Korovin, K. (2024). VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic. In N. Bjørner, M. Heule, & A. Voronkov (Eds.), Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 147–164). https://doi.org/10.29007/kg4v
  Download: PDF (597 KB)
  Projects: ForSmart (2023–2027) / SFB SPyCoDe (2023–2026)
• Superposition with Delayed Unification / Bhayat, A., Schoisswohl, J., & Rawson, M. (2023). Superposition with Delayed Unification. In B. Pientka & C. Tinelli (Eds.), Automated Deduction – CADE 29  29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings (pp. 23–40). Springer. https://doi.org/10.1007/978-3-031-38499-8_2
  Projects: ARTIST (2021–2026) / SFB SPyCoDe (2023–2026)
• Refining Unification with Abstraction / Bhayat, A., Korovin, K., Kovács, L., & Schoisswohl, J. (2023). Refining Unification with Abstraction. In R. Piskac & A. Voronkov (Eds.), Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 36–47). EasyChair EPiC. https://doi.org/10.29007/h65j
  Download: PDF (394 KB)
  Projects: ARTIST (2021–2026) / SFB SPyCoDe (2023–2026)
• ALASCA: Reasoning in Quantified Linear Arithmetic / Korovin, K., Kovács, L., Reger, G., Schoisswohl, J., & Voronkov, A. (2023). ALASCA: Reasoning in Quantified Linear Arithmetic. In S. Sankaranarayanan & N. Sharygina (Eds.), Tools and Algorithms for the Construction and Analysis of Systems (pp. 647–665). Springer. https://doi.org/10.1007/978-3-031-30823-9_33
  Download: PDF (479 KB)
  Projects: ARTIST (2021–2026) / SFB SPyCoDe (2023–2026)
• Inductive Benchmarks for Automated Reasoning / Hajdu, M., Hozzová, P., Kovács, L., Schoisswohl, J., & Voronkov, A. (2021). Inductive Benchmarks for Automated Reasoning. In Intelligent Computer Mathematics. 14th International Conference, CICM 2021, Timisoara, Romania, July 26–31, 2021. Proceedings (pp. 124–129). Springer. https://doi.org/10.34726/1563
  Download: PDF (216 KB)
  Projects: ARTIST (2021–2026) / Symcar (2016–2021)
• Automating Induction by Reflection / Schoisswohl, J., & Kovács, L. (2021). Automating Induction by Reflection. In E. Pimentel & E. Tassi (Eds.), Electronic Proceedings in Theoretical Computer Science (pp. 39–54). EPTCS. https://doi.org/10.4204/eptcs.337.4
• Algorithm selection and instance space analysis for curriculum-based course timetabling / De Coster, A., Musliu, N., Schaerf, A., Schoisswohl, J., & Smith-Miles, K. (2021). Algorithm selection and instance space analysis for curriculum-based course timetabling. Journal of Scheduling, 25(1), 35–58. https://doi.org/10.1007/s10951-021-00701-x
• Induction with Generalization in Superposition Reasoning / Hajdú, M., Hozzová, P., Kovács, L., Schoisswohl, J., & Voronkov, A. (2020). Induction with Generalization in Superposition Reasoning. In Proceedings of the 13th International Conference on Intelligent Computer Mathematics (CICM) (pp. 123–137). Springer. https://doi.org/10.34726/961
  Download: Postprint was published at CICM 2020. (300 KB)
  Projects: DoS-IoT (2019–2020) / Symcar (2016–2021) / SYMELS (2019–2020)
• Automated induction by reflection / Schoisswohl, J. (2020). Automated induction by reflection [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.75342
  Download: PDF (591 KB)