scientific article
From MaRDI portal
Publication:2751378
zbMath0992.68189MaRDI QIDQ2751378
R. Chandra Guru Sekar, Andrei Voronkov, I. V. Ramakrishnan
Publication date: 21 October 2001
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items (31)
A set automaton to locate all pattern matches in a term ⋮ Quantifier simplification by unification in SMT ⋮ LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners ⋮ Aligning concepts across proof assistant libraries ⋮ Multi-completion with termination tools ⋮ Formalization of the resolution calculus for first-order logic ⋮ Pre-indexed Terms for Prolog ⋮ Limited resource strategy in resolution theorem proving ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Combined reasoning by automated cooperation ⋮ Simple and Efficient Clause Subsumption with Feature Vector Indexing ⋮ Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning ⋮ Citius altius fortius ⋮ Efficient instance retrieval with standard and relational path indexing ⋮ Perfect Discrimination Graphs: Indexing Terms with Integer Exponents ⋮ On the Saturation of YAGO ⋮ Building Theorem Provers ⋮ Machine learning guidance for connection tableaux ⋮ Selecting the Selection ⋮ Twee: an equational theorem prover ⋮ GKC: a reasoning system for large knowledge bases ⋮ Maintenance of datalog materialisations revisited ⋮ First order Stålmarck. Universal lemmas through branch merges ⋮ Proof search algorithm in pure logical framework ⋮ A Knuth-Bendix-like ordering for orienting combinator equations ⋮ Subsumption demodulation in first-order theorem proving ⋮ E-matching for Fun and Profit ⋮ An efficient subsumption test pipeline for BS(LRA) clauses ⋮ A complete superposition calculus for primal grammars ⋮ SAT-Inspired Eliminations for Superposition
This page was built for publication:
