On the (In-)Completeness of Destructive Equality Resolution in the Superposition Calculus

Autor: Waldmann, Uwe

Bachmair's and Ganzinger's abstract redundancy concept for the Superposition Calculus justifies almost all operations that are used in superposition provers to delete or simplify clauses, and thus to keep the clause set manageable. Typical examples a

Externí odkaz: http://arxiv.org/abs/2405.03367

Superposition for Lambda-Free Higher-Order Logic

Autor: Bentkamp, Alexander, Blanchette, Jasmin, Cruanes, Simon, Waldmann, Uwe

Publikováno v: Logical Methods in Computer Science, Volume 17, Issue 2 (April 12, 2021) lmcs:6455

We introduce refutationally complete superposition calculi for intentional and extensional clausal $\lambda$-free higher-order logic, two formalisms that allow partial application and applied variables. The calculi are parameterized by a term order t

Externí odkaz: http://arxiv.org/abs/2005.02094

Cancellative Abelian monoids in refutational theorem proving

Autor: Waldmann, Uwe.

Saarbrücken, Univ., Diss., 1997.
Computerdatei im Fernzugriff.

Externí odkaz: http://scidok.sulb.uni-saarland.de/volltexte/2004/243/pdf/UweWaldmann_ProfDrHaraldGanzinger.pdf
http://scidok.sulb.uni-saarland.de/volltexte/2004/243/index.html
http://deposit.ddb.de/cgi-bin/dokserv?idn=972337210

Verification of linear hybrid systems with large discrete state spaces using counterexample-guided abstraction refinement

Autor: Althaus, Ernst, Beber, Björn, Damm, Werner, Disch, Stefan, Hagemann, Willem, Rakow, Astrid, Scholl, Christoph, Waldmann, Uwe, Wirtz, Boris

Publikováno v: In Science of Computer Programming 15 November 2017 148:123-160

A Comprehensive Framework for Saturation Theorem Proving

Autor: Waldmann, Uwe, Tourret, Sophie, Robillard, Simon, Blanchette, Jasmin, Peltier, Nicolas, Sofronie-Stokkermans, Viorica

Publikováno v: Journal of Automated Reasoning, 66(4), 499-539. Springer Netherlands
IJCAR 2020 (Part I) International Joint Conference on Automated Reasoning
IJCAR 2020 (Part I) International Joint Conference on Automated Reasoning, Jun 2020, Paris, France. pp.316-334, ⟨10.1007/978-3-030-51074-9_18⟩
Waldmann, U, Tourret, S, Robillard, S & Blanchette, J 2020, A Comprehensive Framework for Saturation Theorem Proving . in N Peltier & V Sofronie-Stokkermans (eds), Automated Reasoning : 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I . vol. 1, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12166 LNAI, Springer, pp. 316-334, 10th International Joint Conference on Automated Reasoning, IJCAR 2020, Virtual, Online, 1/07/20 . https://doi.org/10.1007/978-3-030-51074-9_18
Automated Reasoning-10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Automated Reasoning
Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I, 1, 316-334
Waldmann, U, Tourret, S, Robillard, S & Blanchette, J 2022, ' A Comprehensive Framework for Saturation Theorem Proving ', Journal of Automated Reasoning, vol. 66, no. 4, pp. 499-539 . https://doi.org/10.1007/s10817-022-09621-7
Automated Reasoning ISBN: 9783030510732
IJCAR (1)
Journal of Automated Reasoning
Journal of Automated Reasoning, 2022, 66 (4), pp.499-539. ⟨10.1007/s10817-022-09621-7⟩
Automated Reasoning

A crucial operation of saturation theorem provers is deletion of subsumed formulas. Designers of proof calculi, however, usually discuss this only informally, and the rare formal expositions tend to be clumsy. This is because the equivalence of dynam

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9ce4f636ee6aa8cdff07937ea4a58d35
https://research.vu.nl/en/publications/04fbca2a-c66f-4cee-a1a1-bca932a6ff60