History and Prospects for First-Order Automated Deduction

DOI10.1007/978-3-319-21401-6_1zbMath1465.03055OpenAlexW1461272771MaRDI QIDQ3454079

David Alan 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

zbMATH Keywords

complexitytheorem provingfirst-order logicresolutionterm rewritinginstance-based methodsmodel-based reasoninggoal-sensitivitysearch space sizes

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) History of mathematical logic and foundations (03-03) History of computer science (68-03) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (4)

A logical reasoning based decision making method for handling qualitative knowledge ⋮ A multi-clause dynamic deduction algorithm based on standard contradiction separation rule ⋮ On structures of regular standard contradictions in propositional logic ⋮ Contradiction separation based dynamic multi-clause synergized automated deduction

Uses Software

• OTTER
• SPASS
• TPTP
• SATCHMO
• DCTP
• iProver-Eq
• iProver
• E Theorem Prover
• Waldmeister
• SRASS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Maslov's inverse method and decidable classes
• Orderings for term-rewriting systems
• Eliminating dublication with the hyper-linking strategy
• A structure-preserving clause form translation
• Seventy-five problems for testing automatic theorem provers
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• Non-Horn clause logic programming without contrapositives
• A simplified problem reduction format
• Non-resolution theorem proving
• The Laplacian with Robin boundary conditions on arbitrary domains
• Ordered semantic hyper-linking
• The generalized projection operator on reflexive Banach spaces and its applications
• A continuous approach to nonlinear integer programming
• A computable filled function used for global minimization
• The model evolution calculus as a first-order DPLL method
• A new filled function method for nonlinear integer programming problem
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• System Description: E 1.8
• On First-Order Model-Based Reasoning
• A Proof Method for Quantification Theory: Its Justification and Realization
• Automated Theorem Proving: After 25 Years
• 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 Unification Algorithm for Associative-Commutative Functions
• Resolution Strategies as Decision Procedures
• The disconnection method
• Semantically guided first-order theorem proving using hyper-linking
• A gradually descent method for discrete global optimization
• A Simplified Format for the Model Elimination Theorem-Proving Procedure
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• iProver-Eq: An Instantiation-Based Theorem Prover with Equality
• Upper bounds on the satisfiability threshold

This page was built for publication: History and Prospects for First-Order Automated Deduction