History and prospects for first-order automated deduction
DOI10.1007/978-3-319-21401-6_1zbMATH Open1465.03055OpenAlexW1461272771MaRDI QIDQ3454079FDOQ3454079
Authors: David A. Plaisted 
Publication date: 2 December 2015
Published in: Automated Deduction - CADE-25 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-21401-6_1
Recommendations
complexityresolutionfirst-order logictheorem provingterm rewritinginstance-based methodsmodel-based reasoninggoal-sensitivitysearch space sizes
History of computer science (68-03) History of mathematical logic and foundations (03-03) Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Title not available (Why is that?)
- Title not available (Why is that?)
- System description: E 1.8
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
- SRASS - A Semantic Relevance Axiom Selection System
- A structure-preserving clause form translation
- Orderings for term-rewriting systems
- Title not available (Why is that?)
- Title not available (Why is that?)
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- A Prolog technology theorem prover: Implementation by an extended Prolog compiler
- Ordered semantic hyper-linking
- The generalized projection operator on reflexive Banach spaces and its applications
- The model evolution calculus as a first-order DPLL method
- A Unification Algorithm for Associative-Commutative Functions
- Title not available (Why is that?)
- The disconnection method
- A Simplified Format for the Model Elimination Theorem-Proving Procedure
- iProver-Eq: An Instantiation-Based Theorem Prover with Equality
- Eliminating dublication with the hyper-linking strategy
- On First-Order Model-Based Reasoning
- Automated Theorem Proving: After 25 Years
- A new filled function method for nonlinear integer programming problem
- Handbook of automated reasoning. In 2 vols
- The Laplacian with Robin boundary conditions on arbitrary domains
- A continuous approach to nonlinear integer programming
- A Proof Method for Quantification Theory: Its Justification and Realization
- Non-Horn clause logic programming without contrapositives
- Non-resolution theorem proving
- Title not available (Why is that?)
- Resolution Strategies as Decision Procedures
- Maslov's inverse method and decidable classes
- Theorem proving in large theories
- A gradually descent method for discrete global optimization
- A simplified problem reduction format
- Title not available (Why is that?)
- Seventy-five problems for testing automatic theorem provers
- Upper bounds on the satisfiability threshold
- A computable filled function used for global minimization
- Title not available (Why is that?)
- Semantically guided first-order theorem proving using hyper-linking
Cited In (7)
- On structures of regular standard contradictions in propositional logic
- Title not available (Why is that?)
- A logical reasoning based decision making method for handling qualitative knowledge
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Contradiction separation based dynamic multi-clause synergized automated deduction
- A multi-clause dynamic deduction algorithm based on standard contradiction separation rule
- Fully reusing clause deduction algorithm based on standard contradiction separation rule
Uses Software
This page was built for publication: History and prospects for first-order automated deduction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3454079)
