Record link: 
http://hdl.handle.net/20.500.12708/192946
-
Title: 
Superposition with Delayed Unification
en
Citation: 
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
-
Publisher DOI: 
10.1007/978-3-031-38499-8_2
-
Publication Type: 
Inproceedings - Full-Paper Contribution
en
Language: 
English
-
Authors: 
Bhayat, Ahmed 
Schoisswohl, Johannes 
Rawson, Michael 
-
Organisational Unit: 
E192-04 - Forschungsbereich Formal Methods in Systems Engineering 
-
Published in: 
Automated Deduction – CADE 29 29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings 
-
ISBN: 
978-3-031-38498-1
-
Volume: 
14132
-
DOI of the book: 
10.1007/978-3-031-38499-8
-
Date (published): 
2-Sep-2023
-
Event name: 
29th International Conference on Automated Deduction 
en
Event date: 
1-Jul-2023 - 4-Jul-2023
-
Event place: 
Roma, Italy
-
Number of Pages: 
18
-
Publisher: 
Springer, Cham
-
Keywords: 
higher-order logic; theorem proving; Superposition
en
Abstract: 
Classically, in saturation-based proof systems, unification has been considered atomic. However, it is also possible to move unification to the calculus level, turning the steps of the unification algorithm into inferences. For calculi that rely on unification procedures returning large or even infinite sets of unifiers, integrating unification into the calculus is an attractive method of dovetailing unification and inference. This applies, for example, to AC-superposition and higher-order superposition. We show that first-order superposition remains complete when moving unification rules to the calculus level. We discuss some of the benefits this has even for standard first-order superposition and provide an experimental evaluation.
en
Project title: 
Automated Reasoning with Theories and Induction for Software Technologies: 101002685 (ERC Consolidator Grant 2020) 
Semantische und kryptografische Grundlagen von Informationssicherheit und Datenschutz durch modulares Design: F 8504 (FWF - Österr. Wissenschaftsfonds) 
-
Research Areas: 
Logic and Computation: 100%
-
Science Branch: 
1020 - Informatik: 100%
-
Appears in Collections:
Conference Paper

Show full item record

Page view(s)

256
checked on Jan 29, 2024

Google ScholarTM

Check

OSZAR »