The following pages link to Automated Deduction - CADE-25 (Q3454078):
Displaying 42 items.
- History and Prospects for First-Order Automated Deduction (Q3454079) (← links)
- Stumbling Around in the Dark: Lessons from Everyday Mathematics (Q3454080) (← links)
- Automated Reasoning in the Wild (Q3454081) (← links)
- Automating Leibniz’s Theory of Concepts (Q3454082) (← links)
- Confluence Competition 2015 (Q3454083) (← links)
- Termination Competition (termCOMP 2015) (Q3454084) (← links)
- Non-E-Overlapping, Weakly Shallow, and Non-Collapsing TRSs are Confluent (Q3454085) (← links)
- CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems (Q3454087) (← links)
- Term Rewriting with Prefix Context Constraints and Bottom-Up Strategies (Q3454088) (← links)
- Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion (Q3454089) (← links)
- Reducing Relative Termination to Dependency Pair Problems (Q3454090) (← links)
- Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers (Q3454091) (← links)
- A Decision Procedure for (Co)datatypes in SMT Solvers (Q3454092) (← links)
- Deciding $$\mathsf {ATL^*}$$ Satisfiability by Tableaux (Q3454093) (← links)
- A Formalisation of Finite Automata Using Hereditarily Finite Sets (Q3454094) (← links)
- SEPIA: Search for Proofs Using Inferred Automata (Q3454097) (← links)
- Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3 (Q3454099) (← links)
- Inductive Beluga: Programming Proofs (Q3454100) (← links)
- SMTtoTPTP – A Converter for Theorem Proving Formats (Q3454101) (← links)
- CTL Model Checking in Deduction Modulo (Q3454102) (← links)
- Quantifier-Free Equational Logic and Prime Implicate Generation (Q3454103) (← links)
- Quantomatic: A Proof Assistant for Diagrammatic Reasoning (Q3454104) (← links)
- Cooperating Proof Attempts (Q3454105) (← links)
- Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses (Q3454106) (← links)
- Beagle – A Hierarchic Superposition Theorem Prover (Q3454107) (← links)
- The Lean Theorem Prover (System Description) (Q3454108) (← links)
- System Description: E.T. 0.1 (Q3454109) (← links)
- Playing with AVATAR (Q3454110) (← links)
- A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited (Q3454111) (← links)
- Exploring Theories with a Model-Finding Assistant (Q3454114) (← links)
- Abstract Interpretation as Automated Deduction (Q3454115) (← links)
- A Uniform Substitution Calculus for Differential Dynamic Logic (Q3454116) (← links)
- Program Synthesis Using Dual Interpretation (Q3454117) (← links)
- Automated Theorem Proving for Assertions in Separation Logic with All Connectives (Q3454118) (← links)
- KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS (Q3454119) (← links)
- KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems (Q3454120) (← links)
- Tableaux Methods for Propositional Dynamic Logics with Separating Parallel Composition (Q3454121) (← links)
- Regular Patterns in Second-Order Unification (Q3454122) (← links)
- Theorem Proving with Bounded Rigid E-Unification (Q3454123) (← links)
- Expressing Symmetry Breaking in DRAT Proofs (Q3454124) (← links)
- MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers (Q3454125) (← links)
- Linear Integer Arithmetic Revisited (Q3454126) (← links)
