Harald Ganzinger’s Legacy: Contributions to Logics and Programming
From MaRDI portal
Publication:4916069
DOI10.1007/978-3-642-37651-1_1zbMath1383.68003OpenAlexW1608222211MaRDI QIDQ4916069
Reinhard Wilhelm, Christoph Weidenbach, Deepak Kapur, Robert Nieuwenhuis, Andrei Voronkov
Publication date: 19 April 2013
Published in: Programming Logics (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-37651-1_1
Biographies, obituaries, personalia, bibliographies (01A70) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) History of computer science (68-03)
Uses Software
Cites Work
- Redundancy criteria for constrained completion
- A completion procedure for conditional equations
- Deciding expressive description logics in the framework of resolution
- A resolution-based decision procedure for \({\mathcal{SHOIQ}}\).
- Increasing modularity and language-independency in automatically generated compilers
- Only prime superpositions need be considered in the Knuth-Bendix completion procedure
- Critical pair criteria for completion
- Order-sorted completion: The many-sorted way
- Superposition theorem proving for abelian groups represented as integer modules
- Refutational theorem proving for hierarchic first-order theories
- Solution of the Robbins problem
- A rewriting approach to satisfiability procedures.
- Superposition with completely built-in abelian groups
- On the undecidability of second-order unification
- Induction = I-axiomatization + first-order consistency.
- Fast term indexing with coded context trees
- Theorem proving with ordering and equality constrained clauses
- Basic paramodulation
- Modular proof systems for partial functions with Evans equality
- Superposition with equivalence reasoning and delayed clause normal form transformation
- Extending ${\cal H}_1$ -Clauses with Path Disequalities
- A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance
- Superposition for fixed domains
- Automated complexity analysis based on ordered resolution
- Ordered chaining calculi for first-order theories of transitive relations
- Superposition Modulo Non-linear Arithmetic
- Unnecessary inferences in associative-commutative completion procedures
- Subterm contextual rewriting
- Integrating Linear Arithmetic into Superposition Calculus
- Labelled Clauses
- System Description: Spass Version 3.0
- Tree Automata with Equality Constraints Modulo Equational Theories
- Superposition Modulo Linear Arithmetic SUP(LA)
- A Technique for Establishing Completeness Results in Theorem Proving with Equality
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Parameterized Specifications: Parameter Passing and Implementation with Respect to Observability
- RIGID REACHABILITY, THE NON-SYMMETRIC FORM OF RIGID E-UNIFICATION
- Monodic temporal resolution
- The axiomatic translation principle for modal logic
- New results on rewrite-based satisfiability procedures
- Automatic recognition of tractability in inference relations
- Computer Science Logic
- Computer Aided Verification
- Theory Instantiation
- A Machine-Oriented Logic Based on the Resolution Principle
- The Concept of Demodulation in Theorem Proving
- Interpolation and Symbol Elimination in Vampire
- On the Saturation of YAGO
- Computer Aided Verification
- Automated Deduction – CADE-19
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
