History and prospects for first-order automated deduction
From MaRDI portal
Publication:3454079
Recommendations
Cites work
- A computable filled function used for global minimization
- A Computing Procedure for Quantification Theory
- A continuous approach to nonlinear integer programming
- A gradually descent method for discrete global optimization
- A machine program for theorem-proving
- A new filled function method for nonlinear integer programming problem
- A Prolog technology theorem prover: Implementation by an extended Prolog compiler
- A Proof Method for Quantification Theory: Its Justification and Realization
- A Simplified Format for the Model Elimination Theorem-Proving Procedure
- A simplified problem reduction format
- A structure-preserving clause form translation
- A Unification Algorithm for Associative-Commutative Functions
- Automated Theorem Proving: After 25 Years
- Eliminating dublication with the hyper-linking strategy
- Handbook of automated reasoning. In 2 vols
- scientific article; zbMATH DE number 4094866 (Why is no real title available?)
- scientific article; zbMATH DE number 3774914 (Why is no real title available?)
- scientific article; zbMATH DE number 1037485 (Why is no real title available?)
- scientific article; zbMATH DE number 1765683 (Why is no real title available?)
- scientific article; zbMATH DE number 3212023 (Why is no real title available?)
- scientific article; zbMATH DE number 3219316 (Why is no real title available?)
- scientific article; zbMATH DE number 3254919 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- iProver-Eq: An Instantiation-Based Theorem Prover with Equality
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
- Maslov's inverse method and decidable classes
- Non-Horn clause logic programming without contrapositives
- Non-resolution theorem proving
- On First-Order Model-Based Reasoning
- Ordered semantic hyper-linking
- Orderings for term-rewriting systems
- Resolution Strategies as Decision Procedures
- Semantically guided first-order theorem proving using hyper-linking
- Seventy-five problems for testing automatic theorem provers
- SRASS - A Semantic Relevance Axiom Selection System
- System description: E 1.8
- The disconnection method
- The generalized projection operator on reflexive Banach spaces and its applications
- The Laplacian with Robin boundary conditions on arbitrary domains
- The model evolution calculus as a first-order DPLL method
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Theorem proving in large theories
- Upper bounds on the satisfiability threshold
Cited in
(7)- Contradiction separation based dynamic multi-clause synergized automated deduction
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- A logical reasoning based decision making method for handling qualitative knowledge
- scientific article; zbMATH DE number 5794052 (Why is no real title available?)
- A multi-clause dynamic deduction algorithm based on standard contradiction separation rule
- On structures of regular standard contradictions in propositional logic
- Fully reusing clause deduction algorithm based on standard contradiction separation rule
Describes a project that uses
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)
