Publication:5679729
From MaRDI portal
zbMath0263.68046MaRDI QIDQ5679729
Chinliang Chang, Richard Chartung Lee
Publication date: 1973
03-01: Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations
68-02: Research exposition (monographs, survey articles) pertaining to computer science
03Bxx: General logic
Related Items
Logical approach to control theory and applications, A nucleus of a theorem-prover described inAlgol-68, On Theorem Proving in Annotated Logics, MRPPS?An interactive refutation proof procedure system for question-answering, Number of models and satisfiability of sets of clauses, Towards a foundation of completion procedures as semidecision procedures, Removing redundancy from a clause, The relative complexity of analytic tableaux and SL-resolution, Parsing as non-Horn deduction, A logic for reasoning with inconsistency, Consensus algorithms for the generation of all maximal bicliques, Purging in an equality data base, Theorem proving with abstraction, An analysis of loop checking mechanisms for logic programs, Resolution for some first-order modal systems, The contraction rule and decision problems for logics without structural rules, Reduction rules for resolution-based systems, Tautologies and positive solvability of linear homogeneous systems, An order-sorted logic for knowledge representation systems, Free fuzzy groups and fuzzy group presentations, A new subsumption method in the connection graph proof procedure, Linear resolution for consequence finding, On the relations between stable and well-founded semantics of logic programs, The completeness of gp-resolution for annotated logics, An implementation of hyper-resolution, A partial evaluator, and its use as a programming tool, Complete problems for deterministic polynomial time, Non-resolution theorem proving, Complete demodulation for automatic theorem proving, Decomposition of linguistic-logical decision models in distributed computing environments, Theorem proving by chain resolution, Prolog technology for default reasoning: proof theory and compilation techniques, On the modelling of search in theorem proving -- towards a theory of strategy analysis, Universal abstract consistency class and universal refutation, Free fuzzy modules and their bases, Completeness issues in RUE-NRF deduction: The undecidability of viability, Gentzen-type systems, resolution and tableaux, Fuzzy operator logic and fuzzy resolution, Automated theorem proving in temporal logic: \(T\)-resolution, A derived algorithm for evaluating \(\varepsilon\)-expressions over abstract sets, On the mechanical derivation of loop invariants, A resolution principle for constrained logics, Hybrid reasoning using universal attachment, Some results on the containment and minimization of (in)equality queries, A logic-based approach to query processing in federated databases, The rue theorem-proving system: The complete set of LIM+ challenge problems, Problem solving by searching for models with a theorem prover, Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures, Ordered model trees: A normal form for disjunctive deductive databases, Enumeration of success patterns in logic programs, An average case analysis of a resolution principle algorithm in mechanical theorem proving., Polynomial-time inference of all valid implications for Horn and related formulae, On renamable Horn and generalized Horn functions, Combining formal derivation search procedures and natural theorem proving techniques in an automated theorem proving system, Solving problems with automated reasoning, expert systems and neural networks, A formal specification of document processing, On Skolemization in constrained logics, A temporal logic for real-time partial ordering with named transactions, Probabilistic conflicts in a search algorithm for estimating posterior probabilities in Bayesian networks, Clause trees: A tool for understanding and implementing resolution in automated reasoning, Computing answers with model elimination, \(\mathcal I\)-SATCHMORE: An improvement of \(\mathcal A\)-SATCHMORE, A fuzzy logic with interval truth values, Deciding the \(E^+\)-class by an a posteriori, liftable order, Linear strategy for Boolean ring based theorem proving, Proofs as schemas and their heuristic use, On ultrafilter logic and special functions, A resolution-based system for symbolic approximate reasoning, Logic inference using formulas with temporal connectives, Inherited extension of many-sorted theories, A method for the synthesis of deducibility conditions for Horn and some other formulas, The achievement of knowledge bases by cycle search., Working with ARMs: Complexity results on atomic representations of Herbrand models, The application of automated reasoning to formal models of combinatorial optimization, A typed resolution principle for deduction with conditional typing theory, Thue trees, Deciding the guarded fragments by resolution, Hypothesis finding based on upward refinement of residue hypotheses., SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy, SATCHMORE: SATCHMO with RElevancy, \(M\)-calculus -- a sequent method for automatic theorem proving, Belief revision, conditional logic and nonmonotonic reasoning, Consistency test for simple specifications of automaton systems, Resolution approach to testing compatibility of interacting automata, A transformation-based synthesis of temporal specification, Determinization of logical specifications of automata, Linear and unit-resulting refutations for Horn theories, Avoiding duplicate proofs with the foothold refinement, Resolution remains hard under equivalence, Polynomial algorithm of limited propositional deduction, Separable resolution method for checking the satisfiability of formulas in the language \({\mathfrak L}\), Counting for satisfiability by inverting resolution, The practicality of generating semantic trees for proofs of unsatisfiability, Improving the time efficiency of proving theorems using a learning mechanism, Unnamed Item, Proof theory in the USSR 1925–1969, Decidable, polynomial-time, and np-complete cases of the isotone bipartite graph problem, New problems complete for nondeterministic log space, Some notes concerning fuzzy logics, ARTIFICIAL INTELLIGENCE—A NEW DISCIPLINE IN THE COMPUTER SCIENCES (A VIEWPOINT), Representations of the language recognition problem for a theorem prover, Application of fuzzy logic to the detection of static hazards in combinational switching systems, Exploiting parallelism: highly competitive semantic tree theorem prover, Parallel inference algorithms for the connection method on systolic arrays, A three-valued approach to default logic, Theorem proving techniques for view deletion in databases, A higher-order interpretation of deductive tableau, Program transformation system based on generalized partial computation
