Harald Ganzinger’s Legacy: Contributions to Logics and Programming (Q4916069): Difference between revisions

@@ Property / cites work @@
+New results on rewrite-based satisfiability procedures
+Normal rank
@@ Property / cites work @@
+Superposition Modulo Linear Arithmetic SUP(LA)
@@ Property / cites work: Superposition Modulo Linear Arithmetic SUP(LA) / rank @@
+Normal rank
@@ Property / cites work @@
+A rewriting approach to satisfiability procedures.
+Normal rank
@@ Property / cites work @@
+Critical pair criteria for completion
@@ Property / cites work: Critical pair criteria for completion / rank @@
+Normal rank
@@ Property / cites work @@
+Rewrite-based Equational Theorem Proving with Selection and Simplification
+Normal rank
@@ Property / cites work @@
+Q4255513
@@ Property / cites work: Q4255513 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4249896
@@ Property / cites work: Q4249896 / rank @@
+Normal rank
@@ Property / cites work @@
+Automated complexity analysis based on ordered resolution
+Normal rank
@@ Property / cites work @@
+Ordered chaining calculi for first-order theories of transitive relations
+Normal rank
@@ Property / cites work @@
+Q4524792
@@ Property / cites work: Q4524792 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751353
@@ Property / cites work: Q2751353 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4264723
@@ Property / cites work: Q4264723 / rank @@
+Normal rank
@@ Property / cites work @@
+Basic paramodulation
@@ Property / cites work: Basic paramodulation / rank @@
+Normal rank
@@ Property / cites work @@
+Q3817580
@@ Property / cites work: Q3817580 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4249897
@@ Property / cites work: Q4249897 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4246725
@@ Property / cites work: Q4246725 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4282593
@@ Property / cites work: Q4282593 / rank @@
+Normal rank
@@ Property / cites work @@
+Refutational theorem proving for hierarchic first-order theories
+Normal rank
@@ Property / cites work @@
+Induction = I-axiomatization + first-order consistency.
+Normal rank
@@ Property / cites work @@
+Monodic temporal resolution
@@ Property / cites work: Monodic temporal resolution / rank @@
+Normal rank
@@ Property / cites work @@
+Superposition Modulo Non-linear Arithmetic
@@ Property / cites work: Superposition Modulo Non-linear Arithmetic / rank @@
+Normal rank
@@ Property / cites work @@
+Q4094350
@@ Property / cites work: Q4094350 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3048295
@@ Property / cites work: Q3048295 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3048294
@@ Property / cites work: Q3048294 / rank @@
+Normal rank
@@ Property / cites work @@
+Increasing modularity and language-independency in automatically generated compilers
+Normal rank
@@ Property / cites work @@
+Q3664415
@@ Property / cites work: Q3664415 / rank @@
+Normal rank
@@ Property / cites work @@
+Parameterized Specifications: Parameter Passing and Implementation with Respect to Observability
+Normal rank
@@ Property / cites work @@
+Q3817656
@@ Property / cites work: Q3817656 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3753472
@@ Property / cites work: Q3753472 / rank @@
+Normal rank
@@ Property / cites work @@
+A completion procedure for conditional equations
@@ Property / cites work: A completion procedure for conditional equations / rank @@
+Normal rank
@@ Property / cites work @@
+Order-sorted completion: The many-sorted way
@@ Property / cites work: Order-sorted completion: The many-sorted way / rank @@
+Normal rank
@@ Property / cites work @@
+Q4329239
@@ Property / cites work: Q4329239 / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-19
@@ Property / cites work: Automated Deduction – CADE-19 / rank @@
+Normal rank
@@ Property / cites work @@
+RIGID REACHABILITY, THE NON-SYMMETRIC FORM OF RIGID E-UNIFICATION
+Normal rank
@@ Property / cites work @@
+Computer Science Logic
@@ Property / cites work: Computer Science Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Theory Instantiation
@@ Property / cites work: Theory Instantiation / rank @@
+Normal rank
@@ Property / cites work @@
+Q2762631
@@ Property / cites work: Q2762631 / rank @@
+Normal rank
@@ Property / cites work @@
+Superposition with completely built-in abelian groups
+Normal rank
@@ Property / cites work @@
+Q4539609
@@ Property / cites work: Q4539609 / rank @@
+Normal rank
@@ Property / cites work @@
+Fast term indexing with coded context trees
@@ Property / cites work: Fast term indexing with coded context trees / rank @@
+Normal rank
@@ Property / cites work @@
+Q4138064
@@ Property / cites work: Q4138064 / rank @@
+Normal rank
@@ Property / cites work @@
+Superposition with equivalence reasoning and delayed clause normal form transformation
+Normal rank
@@ Property / cites work @@
+Modular proof systems for partial functions with Evans equality
+Normal rank
@@ Property / cites work @@
+Interpolation and Symbol Elimination in Vampire
@@ Property / cites work: Interpolation and Symbol Elimination in Vampire / rank @@
+Normal rank
@@ Property / cites work @@
+Deciding expressive description logics in the framework of resolution
+Normal rank
@@ Property / cites work @@
+Superposition for fixed domains
@@ Property / cites work: Superposition for fixed domains / rank @@
+Normal rank
@@ Property / cites work @@
+Q3838762
@@ Property / cites work: Q3838762 / rank @@
+Normal rank
@@ Property / cites work @@
+Tree Automata with Equality Constraints Modulo Equational Theories
+Normal rank
@@ Property / cites work @@
+Q5581665
@@ Property / cites work: Q5581665 / rank @@
+Normal rank
@@ Property / cites work @@
+A resolution-based decision procedure for \({\mathcal{SHOIQ}}\).
+Normal rank
@@ Property / cites work @@
+Only prime superpositions need be considered in the Knuth-Bendix completion procedure
+Normal rank
@@ Property / cites work @@
+Integrating Linear Arithmetic into Superposition Calculus
+Normal rank
@@ Property / cites work @@
+Labelled Clauses
@@ Property / cites work: Labelled Clauses / rank @@
+Normal rank
@@ Property / cites work @@
+Redundancy criteria for constrained completion
@@ Property / cites work: Redundancy criteria for constrained completion / rank @@
+Normal rank
@@ Property / cites work @@
+On the undecidability of second-order unification
@@ Property / cites work: On the undecidability of second-order unification / rank @@
+Normal rank
@@ Property / cites work @@
+Automatic recognition of tractability in inference relations
+Normal rank
@@ Property / cites work @@
+Solution of the Robbins problem
@@ Property / cites work: Solution of the Robbins problem / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Q4264721
@@ Property / cites work: Q4264721 / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem proving with ordering and equality constrained clauses
+Normal rank
@@ Property / cites work @@
+A Technique for Establishing Completeness Results in Theorem Proving with Equality
+Normal rank
@@ Property / cites work @@
+A Machine-Oriented Logic Based on the Resolution Principle
+Normal rank
@@ Property / cites work @@
+Q3150300
@@ Property / cites work: Q3150300 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5624683
@@ Property / cites work: Q5624683 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3150301
@@ Property / cites work: Q3150301 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2723441
@@ Property / cites work: Q2723441 / rank @@
+Normal rank
@@ Property / cites work @@
+The axiomatic translation principle for modal logic
+Normal rank
@@ Property / cites work @@
+Extending ${\cal H}_1$ -Clauses with Path Disequalities
+Normal rank
@@ Property / cites work @@
+Superposition theorem proving for abelian groups represented as integer modules
+Normal rank
@@ Property / cites work @@
+Q2702595
@@ Property / cites work: Q2702595 / rank @@
+Normal rank
@@ Property / cites work @@
+A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance
+Normal rank
@@ Property / cites work @@
+On the Saturation of YAGO
@@ Property / cites work: On the Saturation of YAGO / rank @@
+Normal rank
@@ Property / cites work @@
+Q4938422
@@ Property / cites work: Q4938422 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4539608
@@ Property / cites work: Q4539608 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4263167
@@ Property / cites work: Q4263167 / rank @@
+Normal rank
@@ Property / cites work @@
+The Concept of Demodulation in Theorem Proving
@@ Property / cites work: The Concept of Demodulation in Theorem Proving / rank @@
+Normal rank
@@ Property / cites work @@
+System Description: Spass Version 3.0
@@ Property / cites work: System Description: Spass Version 3.0 / rank @@
+Normal rank
@@ Property / cites work @@
+Subterm contextual rewriting
@@ Property / cites work: Subterm contextual rewriting / rank @@
+Normal rank
@@ Property / cites work @@
+Q3789100
@@ Property / cites work: Q3789100 / rank @@
+Normal rank
@@ Property / cites work @@
+Unnecessary inferences in associative-commutative completion procedures
+Normal rank
@@ Property / cites work @@
+Q3696496
@@ Property / cites work: Q3696496 / rank @@
+Normal rank