The Specialization of Programs by Theorem Proving

DOI10.1137/0202002zbMath0241.68039OpenAlexW1973554267MaRDI QIDQ5652222

No author found.

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

Mathematics Subject Classification ID

Related Items

Modelling the combination of functional and logic programming languages, A kind of logical compilation for knowledge bases, Unfold/fold transformations for disjunctive logic programs, Subsumption and implication, A fixpoint semantics of Horn sentences based on substitution sets, Type data bases with incomplete information, Dynamic backward reasoning systems, A parallel approach for theorem proving in propositional logic, Minimalism, justification and non-monotonicity in deductive databases, Resolution-based approach to compatibility analysis of interacting automata, Using rewriting rules for connection graphs to prove theorems, A sound and complete query evaluation for implicit predicate which is a semantic descriptor of unknown values, Computing minimal models by partial instantiation, Using the tree representation of terms to recognize matching with neural networks, Complexity of resolution proofs and function introduction, Semantics and properties of existential quantifiers in deductive databases, A logic for programming with complex objects, A Prolog technology theorem prover: A new exposition and implementation in Prolog, Determination of \(\alpha \)-resolution in lattice-valued first-order logic \(\mathrm{LF}(X)\), \(\Pi\)-representation: A clause representation for parallel search, \(\alpha\)-resolution principle based on lattice-valued propositional logic \(\text{LP} (X)\), \(\alpha\)-resolution principle based on first-order lattice-valued logic \(\text{LF}(X)\), Fuzzy logic programming, On the complexity of cutting-plane proofs, Maslov's inverse method and decidable classes, Problem representations and formal properties of heuristic search, Recursive query processing: The power of logic, Resolution deduction to detect satisfiability for another class including non-Horn sentences in propositional logic, A new fuzzy resolution principle based on the antonym, The \(Q^*\) algorithm - a search strategy for a deductive question-answering system, A new combination of input and unit deductions for Horn sentences, Fuzzy propositional logic