scientific article; zbMATH DE number 3212023
From MaRDI portal
Publication:5339307
zbMATH Open0131.01201MaRDI QIDQ5339307FDOQ5339307
Authors: Martin Davis 
Publication date: 1963
Title of this publication is not available (Why is that?)
Recommendations
- Eliminating proofs from programs
- Toward mechanical methods for streamlining proofs
- scientific article; zbMATH DE number 1189109
- On Formally Measuring and Eliminating Extraneous Notions in Proofs
- Proof-theoretic validity based on elimination rules
- On the desirability of mechanizing calculational proofs
- scientific article; zbMATH DE number 2102718
- Proof optimization for partial redundancy elimination
- Removing cycles from proofs
Cited In (16)
- A decidable fragment of predicate calculus
- Banishing ultrafilters from our consciousness
- One modification of the ordering strategy in the resolution method
- The strategy challenge in SMT solving
- My Life as a Logician
- On connections and higher-order logic
- Unification theory
- Seventy Years of Computer Science
- Theorem proving with variable-constrained resolution
- History and prospects for first-order automated deduction
- Using rewriting rules for connection graphs to prove theorems
- The unit-clause proof procedure with equality
- A comparative study of several proof procedures
- Beweisalgorithmen für die Prädikatenlogik
- The linked conjunct method for automatic deduction and related search techniques
- Representations of the language recognition problem for a theorem prover
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5339307)
