scientific article; zbMATH DE number 3415409

Chinliang Chang, Richard Chartung Lee

Publication date: 1973

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Research exposition (monographs, survey articles) pertaining to computer science (68-02) General logic (03Bxx)

Related Items

Completion procedures as semidecision procedures, A New Algorithm for Computing Least Generalization of a Set of Atoms, Proof normalization for resolution and paramodulation, Negation with logical variables in conditional rewriting, Goal directed strategies for paramodulation, Proof theory in the USSR 1925–1969, Unnamed Item, Exploiting parallelism: highly competitive semantic tree theorem prover, Decidable, polynomial-time, and np-complete cases of the isotone bipartite graph problem, Parallel inference algorithms for the connection method on systolic arrays, On the strong completion of logic programs, From LP to LP: Programming with constraints, Constructing Craig interpolation formulas, Unnamed Item, On structures of regular standard contradictions in propositional logic, An algorithm for the retrieval of unifiers from discrimination trees, A three-valued approach to default logic, Finding Effective SAT Partitionings Via Black-Box Optimization, Logical approach to control theory and applications, The disconnection method, A tableau calculus for minimal model reasoning, A resolution theorem prover for intuitionistic logic, Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification, A new method for knowledge compilation: The achievement by cycle search, Advanced indexing operations on substitution trees, Semantic trees revisited: Some new completeness results, Path indexing for AC-theories, Optimized encodings of fragments of type theory in first order logic, New problems complete for nondeterministic log space, Unnamed Item, Constructive mathematical descriptions of subject domains, Canonical Ground Horn Theories, The Blossom of Finite Semantic Trees, Some notes concerning fuzzy logics, Theorem proving techniques for view deletion in databases, How to Produce Information About a Given Entity Using Automated Deduction Methods, A higher-order interpretation of deductive tableau, A nucleus of a theorem-prover described inAlgol-68, ARTIFICIAL INTELLIGENCE—A NEW DISCIPLINE IN THE COMPUTER SCIENCES (A VIEWPOINT), Building Theorem Provers, Program transformation system based on generalized partial computation, The Independent Choice Logic and Beyond, The search efficiency of theorem proving strategies, Semantic tableaux with ordering restrictions, On Theorem Proving in Annotated Logics, Using Merging Variables-Based Local Search to Solve Special Variants of MaxSAT Problem, Exact knowledge compilation in predicate calculus: The partial achievement case, A classification of non-liftable orders for resolution, Hyper tableaux, What you always wanted to know about rigid E-unification, A query answering algorithm for Lukaszewicz' general open default theory, Normalization Issues in Mathematical Representations, MRPPS?An interactive refutation proof procedure system for question-answering, Representations of the language recognition problem for a theorem prover, Application of fuzzy logic to the detection of static hazards in combinational switching systems, Completeness results for inequality provers, Inferences for numerical dependencies, On solving the equality problem in theories defined by Horn clauses, Evidence algorithm and inference search in first-order logics, Semantically-guided goal-sensitive reasoning: model representation, Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs, The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem, Multi-layer logic - a predicate logic including data structure as knowledge representation language, A structure-preserving clause form translation, Hierarchical deduction, Resolution on formula-trees, Rewrite method for theorem proving in first order theory with equality, On the decidability of open logic, Inconsistency check of a set of clauses using Petri net reductions, The number of proof lines and the size of proofs in first order logic, History and basic features of the critical-pair/completion procedure, About the Paterson-Wegman linear unification algorithm, Implication of clauses is undecidable, A new reduction rule for the connection graph proof procedure, A Prolog technology theorem prover: Implementation by an extended Prolog compiler, An algorithm to compute circumscription, Filter-based resolution principle for lattice-valued propositional logic LP\((X)\), Optimizing propositional calculus formulas with regard to questions of deducibility, Modal resolution in clausal form, A note on the completeness of resolution without self-resolution, Finite approximatization of languages for representation of system properties: Axiomatization of dependencies, The ILTP problem library for intuitionistic logic, Defining answer classes using resolution refutation, Purging in an equality data base, A unified algorithm for finding \(k\)-IESFs in linguistic truth-valued lattice-valued propositional logic, Construction and learnability of canonical Horn formulas, Theorem proving with abstraction, Information-based distance measures and the canonical reflection of view updates, E-ccc: between ccc and topos, - its expressive power from the viewpoint of data type theory, Inverse subsumption for complete explanatory induction, An extension to linear resolution with selection function, On the decomposition of datalog program mappings, Conditional equational theories and complete sets of transformations, Experiments with resolution-based theorem-proving algorithms, Un-Skolemizing clause sets, Strategies for modal resolution: Results and problems, A simplified problem reduction format, 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, Optimal pattern recognition procedures and their application, Reduction rules for resolution-based systems, Number of models and satisfiability of sets of clauses, Towards a foundation of completion procedures as semidecision procedures, Tautologies and positive solvability of linear homogeneous systems, An order-sorted logic for knowledge representation systems, Removing redundancy from a clause, Free fuzzy groups and fuzzy group presentations, A new subsumption method in the connection graph proof procedure, Linear resolution for consequence finding, The relative complexity of analytic tableaux and SL-resolution, On the relations between stable and well-founded semantics of logic programs, Parsing as non-Horn deduction, A logic for reasoning with inconsistency, The completeness of gp-resolution for annotated logics, Reasoning about conditional probabilities in a higher-order-logic theorem prover, A sound and complete model-generation procedure for consistent and confidentiality-preserving databases, Consensus algorithms for the generation of all maximal bicliques, An implementation of hyper-resolution, A partial evaluator, and its use as a programming tool, Total correctness in nonstandard logics of programs, Complete problems for deterministic polynomial time, Unification in a combination of arbitrary disjoint equational theories, Non-resolution theorem proving, Complete demodulation for automatic theorem proving, Automation methods for logical derivation and their application in the control of dynamic and intelligent systems, On an unsatisfiability-satisfiability prover, Decomposition of linguistic-logical decision models in distributed computing environments, Compiling a default reasoning system into Prolog, An efficient strategy for non-Horn deductive databases, The semantics of incomplete databases as an expression of preferences, Negation by default and unstratifiable logic programs, Using forcing to prove completeness of resolution and paramodulation, Theorem-proving with resolution and superposition, On the relation between resolution based and completion based theorem proving, 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, \((\alpha, \beta)\)-ordered linear resolution of intuitionistic fuzzy propositional logic, Proof search algorithm in pure logical framework, Completeness of hyper-resolution via the semantics of disjunctive logic programs, A simple deduction method for modal logic, Free fuzzy modules and their bases, Completeness issues in RUE-NRF deduction: The undecidability of viability, Gentzen-type systems, resolution and tableaux, Refutational theorem proving using term-rewriting systems, Fuzzy operator logic and fuzzy resolution, Plausible inferences and plausible reasoning, Equational methods in first order predicate calculus, A resolution rule for well-formed formulae, The reliability of reasoning with unreliable arguments, A relevance restriction strategy for automated deduction, Maximal unifiable subsets and minimal non-unifiable subsets, Complete problems in the first-order predicate calculus, A resolution principle for constrained logics, Hypothesis finding based on upward refinement of residue hypotheses., Hybrid reasoning using universal attachment, Some results on the containment and minimization of (in)equality queries, On preprocessing techniques and their impact on propositional model counting, SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy, 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, The universe of propositional approximations, Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures, Alternating two-way AC-tree automata, Ordered model trees: A normal form for disjunctive deductive databases, SATCHMORE: SATCHMO with RElevancy, 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, \(M\)-calculus -- a sequent method for automatic theorem proving, Counting for satisfiability by inverting resolution, A tetrachotomy of ontology-mediated queries with a covering axiom, Belief revision, conditional logic and nonmonotonic reasoning, The model evolution calculus as a first-order DPLL method, Consistency test for simple specifications of automaton systems, Resolution approach to testing compatibility of interacting automata, A transformation-based synthesis of temporal specification, Combining formal derivation search procedures and natural theorem proving techniques in an automated theorem proving system, Determinization of logical specifications of automata, Automatic synthesis of logical models for order-sorted first-order theories, Solving problems with automated reasoning, expert systems and neural networks, A formal specification of document processing, Formalization of the resolution calculus for first-order logic, On the relationship between CWA, minimal model, and minimal herbrand model semantics, Enhancing the inference mechanism of Nilsson's probabilistic logic, Logical-optimization approach to pursuit problems for a group of targets, Model of representation and acquisition of new knowledge by an autonomous intelligent robot based on the logic of conditionally dependent predicates, On Skolemization in constrained logics, Answering atomic queries in indefinite deductive databases, Linear and unit-resulting refutations for Horn theories, Craig interpolation with clausal first-order tableaux, Avoiding duplicate proofs with the foothold refinement, On First-Order Model-Based Reasoning, 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, Contradiction separation based dynamic multi-clause synergized automated deduction, A reduction method and qualitative analysis of dynamic systems. II, Semantically-guided goal-sensitive reasoning: inference system and completeness, Ideal resolution principle for lattice-valued first-order logic based on lattice implication algebra, Resolution remains hard under equivalence, Automatic synthesis of action programs for intelligent robots, Polynomial algorithm of limited propositional deduction, The practicality of generating semantic trees for proofs of unsatisfiability, \(\mathcal I\)-SATCHMORE: An improvement of \(\mathcal A\)-SATCHMORE, Separable resolution method for checking the satisfiability of formulas in the language \({\mathfrak L}\), Towards a unified model of search in theorem-proving: subgoal-reduction strategies, Partition-based logical reasoning for first-order and propositional theories, An approach to automatic deductive synthesis of functional programs, Generalized Conflict-Clause Strengthening for Satisfiability Solvers, The reference ontology of collective behavior of autonomous agents and its extensions, Improving the time efficiency of proving theorems using a learning mechanism, DL-LINK: A CONCEPTUAL CLUSTERING ALGORITHM FOR INDEXING DESCRIPTION LOGICS KNOWLEDGE BASES, Cut rule for the resolution method, Decidability of the Class E by Maslov’s Inverse Method, Formalizing a fragment of combinatorics on words, On ultrafilter logic and special functions, Foundation of credibilistic logic, Weak logic theory, \(\Lambda\)-resolution and interpretation of \(\Lambda\)-implication in fuzzy operator logic, Proving semantic properties as first-order satisfiability, A resolution-based system for symbolic approximate reasoning, Logic inference using formulas with temporal connectives, Inherited extension of many-sorted theories, P-Prolog: A parallel logic language based on exclusive relation, Formalization of the Resolution Calculus for First-Order Logic, Combining Consistency and Confidentiality Requirements in First-Order Databases, CWA Extensions to Multi-Valued Logics, Horn equational theories and paramodulation, Canonical Horn Representations and Query Learning, On equational theories, unification, and (un)decidability, A fuzzy logic with interval truth values, Deciding the \(E^+\)-class by an a posteriori, liftable order, The linked conjunct method for automatic deduction and related search techniques, Linear strategy for Boolean ring based theorem proving, FTClogic: fuzzy temporal constraint logic, Proofs as schemas and their heuristic use, A method for the synthesis of deducibility conditions for Horn and some other formulas, Embedding deductive capabilities in relational database systems, 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, Encoding First Order Proofs in SMT, Set of support, demodulation, paramodulation: a historical perspective, Thue trees, Deciding the guarded fragments by 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