- 2023
- Yasmine Briefs
, Hendrik Leidinger, Christoph Weidenbach:
KBO Constraint Solving Revisited. FroCoS 2023: 81-98 - Martin Bromberger, Lorenz Leutgeb, Christoph Weidenbach:
Symbolic Model Construction for Saturated Constrained Horn Clauses. FroCoS 2023: 137-155 - Chad E. Brown, Adam Pease, Josef Urban:
Translating SUMO-K to Higher-Order Set Theory. FroCoS 2023: 255-274 - Giorgio Cignarale, Roman Kuznets, Hugo Rincon Galeana, Ulrich Schmid:
Logic of Communication Interpretation: How to Not Get Lost in Translation. FroCoS 2023: 119-136 - Burak Ekici, Arjun Viswanathan, Yoni Zohar, Cesare Tinelli, Clark W. Barrett:
Formal Verification of Bit-Vector Invertibility Conditions in Coq. FroCoS 2023: 41-59 - Ryota Haga, Yuki Kagaya, Takahito Aoto:
A Critical Pair Criterion for Level-Commutation of Conditional Term Rewriting Systems. FroCoS 2023: 99-116 - Nils Lommen, Jürgen Giesl:
Targeting Completeness: Using Closed Forms for Size Bounds of Integer Programs. FroCoS 2023: 3-22 - Sibylle Möhle:
An Abstract CNF-to-d-DNNF Compiler Based on Chronological CDCL. FroCoS 2023: 195-213 - Visa Nummelin, Jasmin Blanchette, Sander R. Dahmen:
Recurrence-Driven Summations in Automated Deduction. FroCoS 2023: 23-40 - Teppei Saito, Nao Hirokawa:
Weighted Path Orders Are Semantic Path Orders. FroCoS 2023: 63-80 - Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett:
Combining Finite Combination Properties: Finite Models and Busy Beavers. FroCoS 2023: 159-175 - Olle Torstensson, Tjark Weber:
Hammering Floating-Point Arithmetic. FroCoS 2023: 217-235 - Farah Al Wardani, Kaustuv Chaudhuri, Dale Miller:
Formal Reasoning Using Distributed Assertions. FroCoS 2023: 176-194 - Liao Zhang, Lasse Blaauwbroek, Cezary Kaliszyk, Josef Urban:
Learning Proof Transformations and Its Applications in Interactive Theorem Proving. FroCoS 2023: 236-254 - Uli Sattler, Martin Suda:
Frontiers of Combining Systems - 14th International Symposium, FroCoS 2023, Prague, Czech Republic, September 20-22, 2023, Proceedings. Lecture Notes in Computer Science 14279, Springer 2023, ISBN 978-3-031-43368-9 [contents] - 2021
- Franz Baader, Oliver Fernández Gil, Maryam Rostamigiv:
Restricted Unification in the DL ℱ0. FroCoS 2021: 81-97 - Peter Baumgartner:
Combining Event Calculus and Description Logic Reasoning via Logic Programming. FroCoS 2021: 98-117 - Filippo Bigarella, Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Martin Jonás, Marco Roveri, Roberto Sebastiani, Patrick Trentin:
Optimization Modulo Non-linear Arithmetic via Incremental Linearization. FroCoS 2021: 213-231 - Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Markus Krötzsch, Christoph Weidenbach:
A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic. FroCoS 2021: 3-24 - Antoine Defourné:
Improving Automation for Higher-Order Proof Steps. FroCoS 2021: 139-153 - Serdar Erbatur, Andrew M. Marshall, Christophe Ringeissen:
Non-disjoint Combined Unification and Closure by Equational Paramodulation. FroCoS 2021: 25-42 - Pascal Fontaine, Hans-Jörg Schurr:
Quantifier Simplification by Unification in SMT. FroCoS 2021: 232-249 - Zarathustra Amadeus Goertzel, Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban:
Fast and Slow Enigmas and Parental Guidance. FroCoS 2021: 173-191 - Hai Lin, Christopher Lynch:
Formal Analysis of Symbolic Authenticity. FroCoS 2021: 271-286 - Hai Lin, Christopher Lynch, Andrew M. Marshall, Catherine A. Meadows, Paliath Narendran, Veena Ravishankar, Brandon Rozek:
Algorithmic Problems in the Symbolic Approach to the Verification of Automatically Synthesized Cryptosystems. FroCoS 2021: 253-270 - Dennis Peuter, Viorica Sofronie-Stokkermans:
Symbol Elimination and Applications to Parametric Entailment Problems. FroCoS 2021: 43-62 - Laine E. Rumreich, Paolo A. G. Sivilotti:
Formal Verification of a Java Component Using the RESOLVE Framework. FroCoS 2021: 287-305 - Mostafa Sakr, Renate A. Schmidt:
Semantic Forgetting in Expressive Description Logics. FroCoS 2021: 118-136 - K. Subramani, Piotr Wojciechowski, Alvaro Velasquez:
On the Copy Complexity of Width 3 Horn Constraint Systems. FroCoS 2021: 63-78 - Martin Suda:
Vampire with a Brain Is a Good ITP Hammer. FroCoS 2021: 192-209
