researchr
explore
Tags
Journals
Conferences
Authors
Profiles
Groups
calendar
New Conferences
Events
Deadlines
search
search
You are not signed in
Sign in
Sign up
Links
Filter by Year
[-]
OR
AND
NOT
1
1980
1982
1984
1986
1988
1990
1992
1994
1996
1997
1998
1999
2000
2001
2002
2003
2004
2005
2006
2007
2008
2009
2010
2011
2012
2013
2014
2015
2016
2017
2018
2019
2020
2021
2022
2023
Filter by Tag
[+]
OR
AND
NOT
1
algebra
C++
Meta-Environment
Prolog
analysis
completeness
constraints
e-science
graph-rewriting
logic
logic programming
meta-model
meta-objects
modal logic
programming
rewriting
rule-based
rules
search
termination
Filter by Author
[+]
OR
AND
NOT
1
Aart Middeldorp
Alan Bundy
Andrei Voronkov
André Platzer
Cesare Tinelli
Christoph Benzmüller
Christoph Weidenbach
David A. Plaisted
Deepak Kapur
Frank Pfenning
Franz Baader
Geoff Sutcliffe
Giles Reger
Jasmin Christian Blanchette
Josef Urban
Jürgen Giesl
Nicolas Peltier
Peter Baumgartner
Rajeev Goré
Renate A. Schmidt
Filter by Top terms
[+]
OR
AND
NOT
1
automated
deduction
description
first
logic
logics
model
order
proof
proofs
prover
proving
reasoning
resolution
system
systems
theorem
unification
using
verification
CADE (cade)
Editions
Publications
Viewing Publication 1 - 100 from 2016
2023
A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification)
Yu-Fang Chen 0001
,
Philipp Rümmer
,
Wei-Lun Tsai
.
cade 2023
:
170-189
[doi]
Proceedings of the 4th International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2022) affiliated with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022), Haifa, Israel, August 11, 2022
Christoph Benzmüller
,
Jens Otten
, editors,
Volume 3326 of
CEUR Workshop Proceedings
, CEUR-WS.org,
2023.
[doi]
Certified Core-Guided MaxSAT Solving
Jeremias Berg
,
Bart Bogaerts 0001
,
Jakob Nordström
,
Andy Oertel
,
Dieter Vandesande
.
cade 2023
:
1-22
[doi]
Superposition with Delayed Unification
Ahmed Bhayat
,
Johannes Schoisswohl
,
Michael Rawson 0001
.
cade 2023
:
23-40
[doi]
On Incremental Pre-processing for SMT
Nikolaj Bjørner
,
Katalin Fazekas
.
cade 2023
:
41-60
[doi]
Verified Given Clause Procedures
Jasmin Blanchette
,
Qi Qiu
,
Sophie Tourret
.
cade 2023
:
61-77
[doi]
Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates
Bernard Boigelot
,
Pascal Fontaine
,
Baptiste Vergain
.
cade 2023
:
542-559
[doi]
QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
Maria Paola Bonacina
,
Stéphane Graham-Lengrand
,
Christophe Vauthier
.
cade 2023
:
78-95
[doi]
Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
Marvin Brieger
,
Stefan Mitsch
,
André Platzer
.
cade 2023
:
96-115
[doi]
SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning
Martin Bromberger
,
Chaahat Jain
,
Christoph Weidenbach
.
cade 2023
:
134-152
[doi]
An Isabelle/HOL Formalization of the SCL(FOL) Calculus
Martin Bromberger
,
Martin Desharnais
,
Christoph Weidenbach
.
cade 2023
:
116-133
[doi]
Formal Reasoning About Influence in Natural Sciences Experiments
Florian Bruse
,
Martin Lange
,
Sören Möller
.
cade 2023
:
153-169
[doi]
SAT-Based Subsumption Resolution
Robin Coutelier
,
Laura Kovács
,
Michael Rawson 0001
,
Jakob Rath
.
cade 2023
:
190-206
[doi]
Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness
Guilherme Vicentin de Toledo
,
Yoni Zohar
,
Clark W. Barrett
.
cade 2023
:
522-541
[doi]
Reasoning About Regular Properties: A Comparative Study
Tomás Fiedor
,
Lukás Holík
,
Martin Hruska
,
Adam Rogalewicz
,
Juraj Síc
,
Pavol Vargovcík
.
cade 2023
:
286-306
[doi]
A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper)
Mathias Fleury
,
Peter Lammich
.
cade 2023
:
207-219
[doi]
Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper)
Florian Frohn
,
Jürgen Giesl
.
cade 2023
:
220-233
[doi]
COOL 2 - A Generic Reasoner for Modal Fixpoint Logics (System Description)
Oliver Görlitz
,
Daniel Hausmann 0001
,
Merlin Humml
,
Dirk Pattinson
,
Simon Prucker
,
Lutz Schröder
.
cade 2023
:
234-247
[doi]
Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT
Elisabeth Henkel
,
Jochen Hoenicke
,
Tanja Schindler
.
cade 2023
:
248-265
[doi]
Proving Termination of C Programs with Lists
Jera Hensel
,
Jürgen Giesl
.
cade 2023
:
266-285
[doi]
Program Synthesis in Saturation
Petra Hozzová
,
Laura Kovács
,
Chase Norman
,
Andrei Voronkov
.
cade 2023
:
307-324
[doi]
A Uniform Formalisation of Three-Valued Logics in Bisequent Calculus
Andrzej Indrzejczak
,
Yaroslav I. Petrukhin
.
cade 2023
:
325-343
[doi]
Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs
Jan-Christoph Kassing
,
Jürgen Giesl
.
cade 2023
:
344-364
[doi]
Verification of NP-Hardness Reduction Functions for Exact Lattice Problems
Katharina Kreuzer
,
Tobias Nipkow
.
cade 2023
:
365-381
[doi]
Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic
Cláudia Nalon
,
Ullrich Hustadt
,
Fabio Papacchini
,
Clare Dixon
.
cade 2023
:
382-400
[doi]
Left-Linear Completion with AC Axioms
Johannes Niederhauser
,
Nao Hirokawa
,
Aart Middeldorp
.
cade 2023
:
401-418
[doi]
+
Dennis Peuter
,
Viorica Sofronie-Stokkermans
,
Sebastian Thunert
.
cade 2023
:
419-437
[doi]
Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings
Brigitte Pientka
,
Cesare Tinelli
, editors,
Volume 14132 of
Lecture Notes in Computer Science
, Springer,
2023.
[doi]
Theorem Proving in Dependently-Typed Higher-Order Logic
Colin Rothgang
,
Florian Rabe 0001
,
Christoph Benzmüller
.
cade 2023
:
438-455
[doi]
Towards Fast Nominal Anti-unification of Letrec-Expressions
Manfred Schmidt-Schauß
,
Daniele Nantes Sobrinho
.
cade 2023
:
456-473
[doi]
Confluence Criteria for Logically Constrained Rewrite Systems
Jonas Schöpf
,
Aart Middeldorp
.
cade 2023
:
474-490
[doi]
Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory
Lukas Stevens
.
cade 2023
:
491-508
[doi]
An Experimental Pipeline for Automated Reasoning in Natural Language (Short Paper)
Tanel Tammet
,
Priit Järv
,
Martin Verrev
,
Dirk Draheim
.
cade 2023
:
509-521
[doi]
Incremental Rewriting Modulo SMT
Gerald Whitters
,
Vivek Nigam
,
Carolyn L. Talcott
.
cade 2023
:
560-576
[doi]
Iscalc: An Interactive Symbolic Computation Framework (System Description)
Bohua Zhan
,
Yuheng Fan
,
Weiqiang Xiong
,
Runqing Xu
.
cade 2023
:
577-589
[doi]
2022
Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description)
Martin Suda 0001
.
cade 2022
:
659-667
[doi]
Rensets and Renaming-Based Recursion for Syntax with Bindings
Andrei Popescu 0001
.
cade 2022
:
618-639
[doi]
Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)
Francisco Durán 0001
,
Steven Eker
,
Santiago Escobar 0001
,
Narciso Martí-Oliet
,
José Meseguer
,
Rubén Rubio
,
Carolyn L. Talcott
.
cade 2022
:
529-540
[doi]
On Eventual Non-negativity and Positivity for the Weighted Sum of Powers of Matrices
S. Akshay 0001
,
Supratik Chakraborty
,
Debtanu Pal
.
cade 2022
:
671-690
[doi]
Term Orderings for Non-reachability of (Conditional) Rewriting
Akihisa Yamada 0002
.
cade 2022
:
248-267
[doi]
Cyclic Proofs, Hypersequents, and Transitive Closure Logic
Anupam Das 0002
,
Marianna Girlando
.
cade 2022
:
509-528
[doi]
Ground Joinability and Connectedness in the Superposition Calculus
André Duarte 0002
,
Konstantin Korovin
.
cade 2022
:
169-187
[doi]
Reasoning About Vectors Using an SMT Theory of Sequences
Ying Sheng 0007
,
Andres Nötzli
,
Andrew Reynolds 0001
,
Yoni Zohar
,
David L. Dill
,
Wolfgang Grieskamp
,
Junkil Park
,
Shaz Qadeer
,
Clark W. Barrett
,
Cesare Tinelli
.
cade 2022
:
125-143
[doi]
Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts
Elvira Albert
,
Pablo Gordillo
,
Alejandro Hernández-Cerezo
,
Clara Rodríguez-Núñez
,
Albert Rubio
.
cade 2022
:
3-7
[doi]
Evonne: Interactive Proof Visualization for Description Logics (System Description)
Christian Alrabbaa
,
Franz Baader
,
Stefan Borgwardt
,
Raimund Dachselt
,
Patrick Koopmann
,
Julián Méndez
.
cade 2022
:
271-280
[doi]
Flexible Proof Production in an Industrial-Strength SMT Solver
Haniel Barbosa
,
Andrew Reynolds 0001
,
Gereon Kremer
,
Hanna Lachnitt
,
Aina Niemetz
,
Andres Nötzli
,
Alex Ozdemir
,
Mathias Preiner
,
Arjun Viswanathan
,
Scott Viteri
,
Yoni Zohar
,
Cesare Tinelli
,
Clark W. Barrett
.
cade 2022
:
15-35
[doi]
Sequent Calculi for Choice Logics
Michael Bernreiter
,
Anela Lolic
,
Jan Maly 0001
,
Stefan Woltran
.
cade 2022
:
331-349
[doi]
Non-associative, Non-commutative Multi-modal Linear Logic
Eben Blaisdell
,
Max I. Kanovich
,
Stepan L. Kuznetsov
,
Elaine Pimentel
,
Andre Scedrov
.
cade 2022
:
449-467
[doi]
Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings
Jasmin Blanchette
,
Laura Kovács
,
Dirk Pattinson
, editors,
Volume 13385 of
Lecture Notes in Computer Science
, Springer,
2022.
[doi]
Decision Problems in a Logic for Reasoning About Reconfigurable Distributed Systems
Marius Bozga
,
Lucas Bueri
,
Radu Iosif
.
cade 2022
:
691-711
[doi]
An Efficient Subsumption Test Pipeline for BS(LRA) Clauses
Martin Bromberger
,
Lorenz Leutgeb
,
Christoph Weidenbach
.
cade 2022
:
147-168
[doi]
Lash 1.0 (System Description)
Chad E. Brown
,
Cezary Kaliszyk
.
cade 2022
:
350-358
[doi]
Paraconsistent Gödel Modal Logic
Marta Bílková
,
Sabine Frittella
,
Daniil Kozhemiachenko
.
cade 2022
:
429-448
[doi]
Goéland: A Concurrent Tableau-Based Theorem Prover (System Description)
Julie Cailler
,
Johann Rosain
,
David Delahaye
,
Simon Robillard
,
Hinde-Lilia Bouziane
.
cade 2022
:
359-368
[doi]
Actions over Core-Closed Knowledge Bases
Claudia Cauli
,
Magdalena Ortiz
,
Nir Piterman
.
cade 2022
:
281-299
[doi]
Reasoning in Non-normal Modal Description Logics
Tiziano Dalmonte
,
Andrea Mazzullo
,
Ana Ozaki
.
cade 2018
:
28-45
[doi]
Towards a Coq Formalization of a Quantified Modal Logic
Ana de Almeida Borges
.
cade 2018
:
13-27
[doi]
From the Universality of Mathematical Truth to the Interoperability of Proof Systems
Gilles Dowek
.
cade 2022
:
8-11
[doi]
* Model Checking for Data-Aware Dynamic Systems with Arithmetic
Paolo Felli
,
Marco Montali
,
Sarah Winkler
.
cade 2022
:
36-56
[doi]
SAT-Based Proof Search in Intermediate Propositional Logics
Camillo Fiorentini
,
Mauro Ferrari 0002
.
cade 2022
:
57-74
[doi]
Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description)
Florian Frohn
,
Jürgen Giesl
.
cade 2022
:
712-722
[doi]
Implicit Definitions with Differential Equations for KeYmaera X - (System Description)
James Gallicchio
,
Yong Kiam Tan
,
Stefan Mitsch
,
André Platzer
.
cade 2022
:
723-733
[doi]
Finite Two-Dimensional Proof Systems for Non-finitely Axiomatizable Logics
Vitor Greati
,
João Marcos 0001
.
cade 2022
:
640-658
[doi]
Semantic Relevance
Fajar Haifani
,
Christoph Weidenbach
.
cade 2022
:
208-227
[doi]
EL via Translation to FOL
Fajar Haifani
,
Patrick Koopmann
,
Sophie Tourret
,
Christoph Weidenbach
.
cade 2022
:
188-207
[doi]
Binary Codes that Do Not Preserve Primitivity
Stepan Holub
,
Martin Raska
,
Stepán Starosta
.
cade 2022
:
369-387
[doi]
Clause Redundancy and Preprocessing in Maximum Satisfiability
Hannes Ihalainen
,
Jeremias Berg
,
Matti Järvisalo
.
cade 2022
:
75-94
[doi]
Leśniewski's Ontology - Proof-Theoretic Characterization
Andrzej Indrzejczak
.
cade 2022
:
541-558
[doi]
Intuitionistic Derivability in Anderson's Variant of the Ontological Argument
Annika Kanckos
.
cade 2018
:
46-63
[doi]
Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description)
Gereon Kremer
,
Andrew Reynolds 0001
,
Clark W. Barrett
,
Cesare Tinelli
.
cade 2022
:
95-105
[doi]
A Framework for Approximate Generalization in Quantitative Theories
Temur Kutsia
,
Cleopatra Pau
.
cade 2022
:
578-596
[doi]
Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices
Ori Lahav
,
Yoni Zohar
.
cade 2022
:
468-485
[doi]
SCL(EQ): SCL for First-Order Logic with Equality
Hendrik Leidinger
,
Christoph Weidenbach
.
cade 2022
:
228-247
[doi]
Do Lawyers Use Automated Reasoning? (invited paper)
Tomer Libal
.
cade 2018
:
1-10
[doi]
Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops
Nils Lommen
,
Fabian Meyer
,
Jürgen Giesl
.
cade 2022
:
734-754
[doi]
Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers
Chaitanya Mangla
,
Sean B. Holden
,
Lawrence C. Paulson
.
cade 2022
:
559-577
[doi]
Formula Simplification via Invariance Detection by Algebraically Indexed Types
Takuya Matsuzaki
,
Tomohiro Fujita
.
cade 2022
:
388-406
[doi]
Local Reductions for the Modal Cube
Cláudia Nalon
,
Ullrich Hustadt
,
Fabio Papacchini
,
Clare Dixon
.
cade 2022
:
486-505
[doi]
(Re)moving Quantifiers to Simplify Parameterised Boolean Equation Systems
Thomas Neele
.
cade 2018
:
64-80
[doi]
Advancing Automated Theorem Proving for the Modal Logics D and S5
Jens Otten
.
cade 2018
:
81-91
[doi]
Automated Verification of Deontic Correspondences in Isabelle/HOL - First Results
Xavier Parent
,
Christoph Benzmüller
.
cade 2018
:
92-108
[doi]
Guiding an Automated Theorem Prover with Neural Rewriting
Jelle Piepenbrock
,
Tom Heskes
,
Mikolás Janota
,
Josef Urban
.
cade 2022
:
597-617
[doi]
Preprocessing of Propagation Redundant Clauses
Joseph E. Reeves
,
Marijn J. H. Heule
,
Randal E. Bryant
.
cade 2022
:
106-124
[doi]
Advances and Challenges in the Development and Application of Forgetting Tools (invited talk abstract)
Renate A. Schmidt
.
cade 2018
:
11-12
[doi]
Synthetic Tableaux: Minimal Tableau Search Heuristics
Michal Sochanski
,
Dorota Leszczynska-Jasion
,
Szymon Chlebowski
,
Agata Tomczyk
,
Marcin Jukiewicz
.
cade 2022
:
407-425
[doi]
GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description)
Tanel Tammet
,
Dirk Draheim
,
Priit Järv
.
cade 2022
:
300-309
[doi]
+-Ontology Justifications
Hui Yang
,
Yue Ma
,
Nicole Bidoit
.
cade 2022
:
310-328
[doi]
2021
The Fusemate Logic Programming System
Peter Baumgartner 0001
.
cade 2021
:
589-601
[doi]
Improving ENIGMA-style Clause Selection while Learning From History
Martin Suda 0001
.
cade 2021
:
543-561
[doi]
Multi-Dimensional Interpretations for Termination of Term Rewriting
Akihisa Yamada 0002
.
cade 2021
:
273-290
[doi]
Neural Precedence Recommender
Filip Bártek
,
Martin Suda 0001
.
cade 2021
:
525-542
[doi]
Subformula Linking for Intuitionistic Logic with Application to Type Theory
Kaustuv Chaudhuri
.
cade 2021
:
200-216
[doi]
The Lean 4 Theorem Prover and Programming Language
Leonardo de Moura
,
Sebastian Ullrich
.
cade 2021
:
625-635
[doi]
Efficient SAT-based Proof Search in Intuitionistic Propositional Logic
Camillo Fiorentini
.
cade 2021
:
217-233
[doi]
Tableau-based Decision Procedure for Non-Fregean Logic of Sentential Identity
Joanna Golinska-Pilarek
,
Taneli Huuskonen
,
Michal Zawidzki
.
cade 2021
:
41-57
[doi]
Automatically Building Diagrams for Olympiad Geometry Problems
Ryan Krueger
,
Jesse Michael Han
,
Daniel Selsam
.
cade 2021
:
577-588
[doi]
The Isabelle/Naproche Natural Language Proof Assistant
Adrian De Lon
,
Peter Koepke
,
Anton Lorenzen
,
Adrian Marti
,
Marcel Schütz
,
Makarius Wenzel
.
cade 2021
:
614-624
[doi]
Proof Search and Certificates for Evidential Transactions
Vivek Nigam
,
Giselle Reis
,
Samar Rahmouni
,
Harald Ruess
.
cade 2021
:
234-251
[doi]
Towards the Automatic Mathematician
Markus N. Rabe
,
Christian Szegedy
.
cade 2021
:
25-37
[doi]
Twee: An Equational Theorem Prover
Nicholas Smallbone
.
cade 2021
:
602-613
[doi]
Sign in
or
sign up
to see more results.