The Specialization of Programs by Theorem Proving
From MaRDI portal
Publication:5652222
DOI10.1137/0202002zbMATH Open0241.68039OpenAlexW1973554267MaRDI QIDQ5652222FDOQ5652222
Author name not available (Why is that?)
Publication date: 1973
Published in: SIAM Journal on Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1137/0202002
Cited In (32)
- The \(Q^*\) algorithm - a search strategy for a deductive question-answering system
- Semantics and properties of existential quantifiers in deductive databases
- \(\alpha\)-resolution principle based on first-order lattice-valued logic \(\text{LF}(X)\)
- Using the tree representation of terms to recognize matching with neural networks
- Fuzzy logic programming
- \(\alpha\)-resolution principle based on lattice-valued propositional logic \(\text{LP} (X)\)
- Unfold/fold transformations for disjunctive logic programs
- A kind of logical compilation for knowledge bases
- Maslov's inverse method and decidable classes
- Resolution-based approach to compatibility analysis of interacting automata
- Type data bases with incomplete information
- A new fuzzy resolution principle based on the antonym
- Complexity of resolution proofs and function introduction
- On the complexity of cutting-plane proofs
- Dynamic backward reasoning systems
- A Prolog technology theorem prover: A new exposition and implementation in Prolog
- Recursive query processing: The power of logic
- A sound and complete query evaluation for implicit predicate which is a semantic descriptor of unknown values
- Problem representations and formal properties of heuristic search
- A fixpoint semantics of Horn sentences based on substitution sets
- A new combination of input and unit deductions for Horn sentences
- Modelling the combination of functional and logic programming languages
- Resolution deduction to detect satisfiability for another class including non-Horn sentences in propositional logic
- Determination of \(\alpha \)-resolution in lattice-valued first-order logic \(\mathrm{LF}(X)\)
- A parallel approach for theorem proving in propositional logic
- Using rewriting rules for connection graphs to prove theorems
- Subsumption and implication
- \(\Pi\)-representation: A clause representation for parallel search
- Minimalism, justification and non-monotonicity in deductive databases
- Computing minimal models by partial instantiation
- A logic for programming with complex objects
- Fuzzy propositional logic
This page was built for publication: The Specialization of Programs by Theorem Proving
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5652222)
