yusuke1997/dblp-id-title huggingface dataset:
The Binomial Pricing Model in Finance: A Formalization in Isabelle
Reasoning about Systems of Linear Inequalities
Tutorial on Compilation techniques for Logics
Formal Proof of the Group Law for Edwards Elliptic Curves
A Normal Form for First-Order Temporal Formulae
Panel Discussion: A Mechanically Proof-Checked Encyclopedia of Mathematics: Should We Build One? Can We?
Interpolant Generation for UTVPI
Focused Inductive Theorem Proving
Chain Resolution for the Semantic Web
Semantic Selection of Premisses for Automated Theorem Proving
Efficient Local Reductions to Basic Modal Logic
MOLOG: a Modal PROLOG
Satisfiability Modulo Theories and Assignments
Trie Based Subsumption and Improving the pi-Trie Algorithm
A Randomized Satisfability Procedure for Arithmetic and Uninterpreted Function Symbols
Hyper-Chaining and Knowledge-Based Theorem Proving
Walther Recursion
Highly Parallel Inference Machine
Towards High-Assurance Multiprocessor Virtualisation
Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
How to Clear a Block: Plan Formation in Situational Logic
Theorem Proving with Bounded Rigid E-Unification
System Description: CyNTHIA
Canonical Gentzen-Type Calculi with (n, k)-ary Quantifiers
Nested Resolution
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
An Example of FOL Using Metatheory
Synthesising Graphical Theories
Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II
Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation
The Use of Explicit Plans to Guide Inductive Proofs
Deep Generation of Coq Lemma Names Using Elaborated Terms
Sorted Unification Using Set Constraints
Uniform variable splitting
Model Completeness, Covers and Superposition
A Tableau-Based Theorem Prover for a Decidable Subset of Default Logic
Possible Models Computation and Revision - A Practical Approach
Using Meta-Level Inference for Selective Application of Multiple Rewrite Rules in Algebraic Manipulation
On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results
The use of types in designing unification algorithms: two case studies
Relatively Complete and Efficient Partial Quantifier Elimination
FasTraC: A Decentralized Traffic Control System Based on Logic Programming
Subsumption Algorithms for Three-Valued Geometric Resolution
Proving Information Flow Noninterference by Reusing a Machine-Checked Correctness Proof for Slicing
A Generic Framework for Implicate Generation Modulo Theories
Reasoning with Individuals for the Description Logic SHIQ
A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers
The Lean Theorem Prover (System Description)
Implementing Tableau Calculi Using BDDs: BDDTab System Description
Intuitionistic Layered Graph Logic
Taming Past LTL and Flat Counter Systems
Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols
Intuitionistic Derivability in Anderson's Variant of the Ontological Argument
Two Techniques to Improve Finite Model Search
A Theorem Prover for a Computational Logic
The Search Efficiency of Theorem Proving Strategies
Hyper Tableaux with Equality
A formalization of Static Analyses in System F
Logic Machine Architecture: Kernel Funtions
Using A Generalisation Critic to Find Bisimulations for Coinductive Proofs
Tutorial on High-Performance Theorem Provers: Efficient Implementation and Parallelisation
A Focusing Inverse Method Theorem Prover for First-Order Linear Logic
Heaps and Data Structures: A Challenge for Automated Provers
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
Propositional Temporal Proving with Reductions to a SAT Problem
Quotients of Bounded Natural Functors
Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings
Puzzles and Paradoxes (Abstract)
Basic Syntactic Mutation
Logic between Expressivity and Complexity
Decidable Matching for Convergent Systems (Preliminary Version)
Solving Non-linear Arithmetic
Divvy: An ATP Meta-system Based on Axiom Relevance Ordering
Structuring Metatheory on Inductive Definitions
A Slice-Based Decision Procedure for Type-Based Partial Orders
A Refined Version of General E-Unification
Certifying a Tree Automata Completion Checker
Proof Tactics for a Theory of State Machines in a Graphical Environment
In Which Sense Is Fuzzy Logic a Logic for Vagueness?
Combining Type Theory and Untyped Set Theory
LOIS: an Application of SMT Solvers
The Linked Inference Principle, II: The User's Viewpoint
Automated Reasoning in Quantified Non-Classical Logics, ARQNL@IJCAR 2014, Vienna, Austria, July 23, 2014
ASASP: Automated Symbolic Analysis of Security Policies
How Fuzzy Is My Fuzzy Description Logic?
CSI - A Confluence Tool
A Probabilistic Abduction Engine for Media Interpretation based on Ontologies
Flyspeck I: Tame Graphs
Model Elimination Without Contrapositives
CASC-J4 The 4th IJCAR ATP System Competition
Locality Transfer: From Constrained Axiomatizations to Reachability Predicates
An Environment For Automated Reasoning About Partial Functions
Formalization of Forcing in Isabelle/ZF
Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates
Mechanizing Constructive Proofs (Abstract)
Do Portfolio Solvers Harm?
Canonization for Disjoint Unions of Theories
A Mechanization of Phylogenetic Trees
System for Automated Deduction (SAD): A Tool for Proof Verification
Gibbs Sampling in Probabilistic Description Logics with Deterministic Dependencies
Dynamic Logic as a Uniform Framework for Theorem Proving in Intensional Logic
QUANTLOG: A System for Approximate Reasoning in Inconsistent Formal Systems
A Real-Analytic Approach to Differential-Algebraic Dynamic Logic
On Notions of Inductive Validity for First-Oder Equational Clauses
Partial Recursive Functions in Higher-Order Logic
A Simple Complexity Measurement for Software Verification and Software Testing
Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs
Automata-Based Axiom Pinpointing
Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings
Optimized Reasoning in Description Logics Using Hypertableaux
24 Challenges in Deductive Software Verification
A Theorem Prover Based Approach for SAT-Based Model Checking Certification
: A Resolution-Based Prover for Multimodal K
An Abstraction-Refinement Framework for Reasoning with Large Theories
Deriving Modular Programs from Short Proofs
Towards a Coq Formalization of a Quantified Modal Logic
Associative-Commutative Deduction with Constraints
The Bayesian Description Logic ${\mathcal{BEL}}$
Importing HOL into Isabelle/HOL
Computing Expected Runtimes for Constant Probability Programs
Matching with Distributivity
Str+ve-Subset: The Str+ve-based Subset Prover
System Description: PTTP+GLiDes: Semantically Guided PTTP
Do Lawyers Use Automated Reasoning? (invited paper)
Invited Talk: Embedding Programming Languages in Theorem Provers (Abstract)
A Tableau System for the Description Logic SHIO
Detecting Non-Provable Goals
System Description: GAPT 2.0
Layered Clause Selection for Saturation-Based Theorem Proving
Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation
Workshop on Proof Search in Type-Theoretic Languages (in conjunction with CADE-15 Conference), Lindau, Germany, July 5, 1998
Theories as Types
Proceedings of the Workshop on Bridging the Gap between Human and Automated Reasoning - A workshop of the 25th International Conference on Automated Deduction (CADE-25), Berlin, Germany, August 1, 2015
A Natural Deduction Automated Theorem Proving System
Tool Demonstration of the FLATA Counter Automata Toolset
Learning Domain Knowledge to Improve Theorem Proving
Automatic Program Optimization Through Proof Transformation
Logtk: A Logic ToolKit for Automated Reasoning and its Implementation
RRL: A Rewrite Rule Laboratory
ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback
Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis
Schematic Cut Elimination and the Ordered Pigeonhole Principle
Exporting and Refecting Abstract Metamathematics
Analytica - A Theorem Prover in Mathematica
A New Meta-complexity Theorem for Bottom-Up Logic Programs
Iscalc: An Interactive Symbolic Computation Framework (System Description)
The Complexity of Theorem Proving in Circumscription and Minimal Entailment
Term Orderings for Non-reachability of (Conditional) Rewriting
Preprocessing of Propagation Redundant Clauses
Extending Sledgehammer with SMT Solvers
System Description: Waldmeister - Improvements in Performance and Ease of Use
Saturation-Based Theorem Proving: Past Successes and Future Potential (Abstract)
Algebraic Polynomial-based Synthesis for Abstract Boolean Network Analysis
Using Middle-Out Reasoning to Control the Synthesis of Tail-Recursive Programs
An Efficient Subsumption Test Pipeline for BS(LRA) Clauses
On Interpolation and Symbol Elimination in Theory Extensions
KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
Optimization in SMT with ${\mathcal LA}$ (ℚ) Cost Functions
Scalable Fine-Grained Proofs for Formula Processing
The SMT Execution Service: Features, Fairness, and the Future
Engineering DPLL(T) + Saturation
Learning Preferences for Collaboration
The MODPROF Theorem Prover
Complexity of Combinations of Qualitative Constraint Satisfaction Problems
A Resolution Decision Procedure for Fluted Logic
Context Trees
Covered Clauses Are Not Propagation Redundant
SMT-LIB Sequences and Regular Expressions
E-MaLeS 1.1
INKA: The Next Generation
The SHUNYATA System
A General Inductive Completion Algorithm and Application to Abstract Data Types
Faithful Logic Embeddings in HOL - Deep and Shallow
We know (nearly) nothing!l But can we learn?
Unification in Order-Sorted Algebras with Overloading
Decidable Higher-Order Unification Problems
Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
More Church-Rosser Proofs (in Isabelle/HOL)
Recursive Query Answering with Non-Horn Clauses
Hyper Resolution and Equality Axioms without Function Substitutions
Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings
The Challenges of Evaluating a New Feature in Vampire
The 6th IJCAR ATP System Competition, CASC-J6, June 28, 2012, Manchester, UK
Algorithms, Datastructures, and other Issues in Efficient Automated Deduction
GridTPT: a distributed platform for Theorem Prover Testing
A New DL-Lite N Bool Probabilistic Extension Using Belief
Dual Proof Generation for Quantified Boolean Formulas with a BDD-based Solver
Implementations of Natural Logics
Satisfiability of Compositional Separation Logic with Tree Predicates and Data Constraints
Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems
Reasoning by Symmetry and Function Ordering in Finite Model Generation
Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings
Count and Forget: Uniform Interpolation of $\mathcal{SHQ}$ -Ontologies
P.rex: An Interactive Proof Explainer
Reasoning in Extensional Type Theory with Equality
Satisfiability Modulo Transcendental Functions via Incremental Linearization
Proof Development with OMEGA
Optimizing a BDD-Based Modal Solver
Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop, 2020 co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020), Paris, France, June-July, 2020 (Virtual)
Efficient Certified RAT Verification
Solving Word Problems in Free Algebras Using Complexity Functions
Compositional Proofs with Symbolic Execution
SGGS Theorem Proving: an Exposition
Superposition with Delayed Unification
Cutting Down the TPTP Language (And Others)
An Isabelle/HOL Formalization of the SCL(FOL) Calculus
A Calculus for Generating Ground Explanations
Abstraction-Based Relevancy Testing for Model Elimination
Cut-Simulation in Impredicative Logics
GEOMETER: A Theorem Prover for Algebraic Geometry
KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
A General Clause Theorem Prover
Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning, PAAR-2010, Edinburgh, Scotland, UK, July 14, 2010
Tractable Inference Systems: An Extension with a Deducibility Predicate
A Tableau Calculus for Regular Grammar Logics with Converse
Towards Bit-Width-Independent Proofs in SMT Solvers
SMT-Based System Verification with DVF
Modular Proof Systems for Partial Functions with Weak Equality
Tutorial on High-Performance Automated Theorem Proving
Synthetic Tableaux: Minimal Tableau Search Heuristics
Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving Programs
Mollusc: A General Proof-Development Shell for Sequent-Based Logics
Adding Dynamic Paramodulation to Rewrite Algorithms
NP-Completeness of Refutability by Literal-Once Resolution
Exponential Improvement of Efficient Backtracking: A Strategy for Plan-Based Deduction
System Description: SCOTT-5
GeoGebra and the realgeom Reasoning Tool
A Resolution Calculus for Modal Logics
Logical Support in a Time-Varying Model
Cops and CoCoWeb: Infrastructure for Confluence Tools
Automated Reasoning for Explainable Artificial Intelligence
Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems
A New Combination Procedure for the Word Problem That Generalizes Fusion Decidability Results in Modal Logics
An Implementation of a Dissolution-Based System Employing Theory Links
Hyperparamodulation: A Refinement of Paramodulation
Reasoning Support for OWL-E
An Interpretation of Isabelle/HOL in HOL Light
TFX: The TPTP Extended Typed First-Order Form
Evaluating the Usability of Interactive Verification Systems
Cool - A Generic Reasoner for Coalgebraic Hybrid Logics (System Description)
Towards the Automatic Mathematician
Flexible Proof Production in an Industrial-Strength SMT Solver
Computing Ground Congruence Classes
Non-E-Overlapping, Weakly Shallow, and Non-Collapsing TRSs are Confluent
Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi
Free-Variable Tableaux for Constant-Domain Quantified Modal Logics with Rigid and Non-rigid Designation
An implementation of a tableau theorem prover for modal logics
System Description: GrAnDe 1.0
Dynamic Logic with Trace Semantics
The Applicability of Logic Program Analysis and Transformation to Theorem Proving
FDPLL - A First Order Davis-Putnam-Longeman-Loveland Procedure
The Reflection Theorem: A Study in Meta-theoretic Reasoning
A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance
A Hybrid Method for Probabilistic Satisfiability
Checking Array Bounds by Abstract Interpretation and Symbolic Expressions
SAT Encoding of Unification in ℇℒℋ R + w.r.t. Cycle-Restricted Ontologies
Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
A Tableaux Calculus for Default Intuitionistic Logic
A Refined Resolution Calculus for CTL
Well-Founded Unions
Induction, Invariants, and Abstraction
The Complexity of the Graded µ-Calculus
Solvability of Context Equations with Two Context Variables is Decidable
Generalized Well-founded Semantics for Logic Programs (Extended Abstract)
The Karlsruhe Induction Theorem Proving System
Harpoon: Mechanizing Metatheory Interactively - (System Description)
Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates
A Combinatory Logic Approach to Higher-order E-unification (Extended Abstract)
Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings
Unification in Monoidal Theories
LogAnswer - A Deduction-Based Question Answering System (System Description)
A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo Axioms
A Restriction of Factoring in Binary Resolution
LOOPUS - A Tool for Computing Loop Bounds for C Programs
Efficient General Unification for XOR with Homomorphism
Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs
From Reachability to Temporal Specifications in Cost-Sharing Games
lolliCop - A Linear Logic Implementation of a Lean Connection-Method Theorem Prover for First-Order Classical Logic
Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings
A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms
Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution
Formal Requirements Capturing using VRS system
Logical Engineering with Instance-Based Methods
The Illinois Prover: A General Purpose Resolution Theorem Prover
SAT and SMT Are Still Resolution: Questions and Challenges
MUNCH - Automated Reasoner for Sets and Multisets
Towards Logic-Based Verification of JavaScript Programs
Nominal Confluence Tool
Mechanised Modal Model Theory
Decidable Call by Need Computations in term Rewriting (Extended Abstract)
Termination Analysis by Dependency Pairs and Inductive Theorem Proving
Visibly Linear Temporal Logic
Automated Theorem Proving using the TPTP Process Instruction Language
Semantically Guided First-Order Theorem Proving using Hyper-Linking
The KRIPKE Automated Theorem Proving System
Automated Reasoning in the Wild
SHD-Prover at University of Texas at Austin
Automating Elementary Number-Theoretic Proofs Using Gröbner Bases
Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals
A Fast Algorithm for Uniform Semi-Unification
Understanding Higher Order Unification via Explicit Substitutions and Patterns
Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
The Fusemate Logic Programming System
Reasoning About Concurrency in High-Assurance, High-Performance Software Systems
Invariants and Robustness of BIP Models
Query Processing in Quantitative Logic Programming
Schematic Saturation for Decision and Unification Problems
Optimizing Proof Search in Model Elimination
Pseudo-Propositional Logic
On Generating Small Clause Normal Forms
The PIE Environment for First-Order-Based Proving, Interpolating and Eliminating
Computational Metatheory in Nuprl
Case Inference in Resolution-Based Languages
Simultaneous Paramodulation
Clausal Resolution for Modal Logics of Confluence
Constructing a Normal Form for Property Theory
Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development
Proof by Induction Using Test Sets
Automated Proof of Authentication Protocols in a Logic of Events
A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution
Term Rewriting: Some Experimental Results
Integrating Induction and Coinduction via Closure Operators and Proof Cycles
Ground Joinability and Connectedness in the Superposition Calculus
Verification of Closest Pair of Points Algorithms
Implementing the Meta-Theory of Deductive Systems
Evolving Combinators
Hierarchic Superposition with Weak Abstraction
Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings
Semantic Trees Revisited: Some New Completeness Results
Formal Global Optimisation with Taylor Models
Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings
Labelled Connection-based Proof Search for Multiplicative Intuitionistic
Termination Competition (termCOMP 2015)
Connecting Many-Sorted Theories
Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts
A One-Pass Tableau-Based Workflow Verification Framework
Efficient Checking of Term Ordering Constraints
The Heterogeneous Tool Set (Hets)
Analytic Tableaux for Higher-Order Logic with Choice
COOL 2 - A Generic Reasoner for Modal Fixpoint Logics (System Description)
Deciding Security for Protocols with Recursive Tests
Refinement and Term Synthesis in Loop Invariant Generation
XIsabelle: A System Description
DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL
Complete Monotonic Semantic Path Orderings
One Logic to Use Them All
HipSpec: Automating Inductive Proofs of Program Properties
Bounded Higher-order Unification using Regular Terms
Schemata
Exotic Semi-Ring Constraints
Computing a Complete Basis for Equalities Implied by a System of LRA Constraints
Colors Make Theories Hard
Notions of Knowledge in Combinations of Theories Sharing Constructors
On Explicit Reflection in Theorem Proving and Formal Verification
Make E Smart Again (Short Paper)
Learning from Multiple Proofs: First Experiments
An Improved Method for Adding Equality to Free Variable Semantic Tableaux
A Novel Asynchronous Parallelism Scheme for First-Order Logic
The QMLTP Problem Library for First-Order Modal Logics
Formula Simplification via Invariance Detection by Algebraically Indexed Types
Unification in a Combination of Arbitrary Disjoint Equational Theories
Efficient Well-Definedness Checking
Simplifying Casts and Coercions (Extended Abstract)
Some Relationships between Unification, restricted Unification, and Matching
Flaw Detection in Formal Specifications
A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering That x³=x Implies Ring Commutativity
The KLAUS Automated Deduction System
REVE a Rewrite Rule Laboratory
Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers
Anatomy of Alternating Quantifier Satisfiability (Work in progress)
Lightweight Verification with Dependent Types
Predicate Completion for non-Horn Clause Sets
System Description: SystemOn TPTP
Universal Unification and a Classification of Equational Theories
The Quest for Efficient Boolean Satisfiability Solvers
Playing Hybrid Games with KeYmaera
Learning and Applying Generalised Solutions using Higher Order Resolution
Well-Nested Context Unification
Decidability of Arity-Bounded Higher-Order Matching
OTTER Proofs in Tarskian Geometry
Unification in an Extensional Lambda Calculus with Ordered Function Sorts and Constant Overloading
SAT-Based Subsumption Resolution
An SMT Theory of Fixed-Point Arithmetic
Gödel's Algorithm for Class Formation
Exploring Abstract Algebra in Constructive Type Theory
Experimenting with Deduction Modulo
Automating the Dependency Pair Method
6th International Verification Workshop, VERIFY-2010, Edinburgh, UK, July 20-21, 2010
Automated Deduction - CADE-15, 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings
Automated Deduction of Finite-State Control Programs for Reactive Systems
Dialogues for proof search
Workshop: Automated Deduction in Education
Uniform Traversal Combinators: Definition, Use and Properties
Enlarging the Scope of Applicability of Successful Techniques for Automated Reasoning in Mathematics
Formal Metatheory using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems
An Experiment with "Edinburgh LCF"
The Design of the CADE-16 Inductive Theorem Prover Contest
A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems
A New Formula for the Execution of Categorial Combinators
Searching While Keeping a Trace: The Evolution from Satisfiability to Knowledge Compilation
A Programming Notation for Tactical Reasoning
Model Evolution with Equality Modulo Built-in Theories
The Nuprl Open Logical Environment
Satisfiability Modulo Bounded Checking
MaLARea: a Metasystem for Automated Reasoning in Large Theories
Termination of a Set of Rules Modulo a Set of Equations