Logic Programming and Automated Reasoning

Entailment and disentailment of order-sorted feature constraints.- Computing extensions of default logic - Preliminary report.- Prolog with arrays and bounded quantifications.- Linear 0-1 inequalities and extended clauses.- Search space pruning by checking dynamic term growth.- A proof search system for a modal substructural logic based on labelled deductive systems.- Consistency checking of automata functional specifications.- Yet another application for Toupie: Verification of mutual exclusion algorithms.- Parsing with DCG-terms.- A first order resolution calculus with symmetries.- Ordered paramodulation and resolution as decision procedure.- Static analysis of Prolog with cut.- A new type theory for representing logics.- Verification of Switch-level designs with many-valued logic.- Deciding in HFS-theory via linear integer programming.- The completion of typed logic programs and SLDNF-resolution.- Increasing the versatility of heuristic based theorem provers.- Sequentialization of parallel logic programs with mode analysis.- Refinements and extensions of model elimination.- Executable specifications based on dynamic algebras.- Generic resolution in propositional modal systems.- Optimized translation of multi modal logic into predicate logic.- Default reasoning with a constraint resolution principle.- Non-clausal deductive techniques for computing prime implicants and prime implicates.- Unification under one-sided distributivity with a multiplicative unit.- Unification in Order-Sorted Logic with Term Declarations.- Extracting inheritance hierarchies from Prolog programs: A system based on the inference of type relations.- A comparison of mechanisms for avoiding repetition of subdeductions in chain format linear deduction systems.- Neutralization and preemption inextended logic programs.- MULTLOG: A system for axiomatizing many-valued logics.- SKIL: A system for programming with proofs.- Reasoning about the reals: the marriage of HOL and maple.- System description of LAMBDALG.- Mixing metafor.- A complete axiom system for isomorphism of types in closed categories.- Reasoning, modeling, and component-based technology.