Logic Programming and Automated Reasoning: 4th International Conference, LPAR'93, St.Petersburg, Russia, July 13-20, 1993. ProceedingsLPAR is an international conference series aimed at bringing together researchers interested in logic programming and automated reasoning. The research in logic programming grew out of the research in automated reasoning in the early 1970s. Later, the implementation techniques known from logic programming were used in implementing theorem proving systems. Results from both fields applied to deductive databases. This volume contains the proceedings of LPAR '93, which was organized by the Russian Association for Logic Programming. The volume contains 35 contributed papers selected from 84 submissions, together with an invited paper by Peter Wegner entitled "Reasoning versus modeling in computer science". |
What people are saying - Write a review
We haven't found any reviews in the usual places.
Contents
Entailment and Disentailment of OrderSorted Feature Constraints | 1 |
Computing Extensions of Default Logic Preliminary Report | 19 |
Prolog with Arrays and Bounded Quantifications | 28 |
Linear 01 Inequalities and Extended Clauses | 40 |
Search Space Pruning by Checking Dynamic Term Growth | 52 |
A Proof Search System for a Modal Substructural Logic Based on Labelled Deductive Systems | 64 |
Consistency Checking of Automata Functional Specifications | 76 |
Verification of Mutual Exclusion Algorithms | 86 |
Refinements and Extensions of Model Elimination | 217 |
Executable Specifications based on Dynamic Algebras | 229 |
Generic Resolution in prepositional modal systems | 241 |
Optimized Translation of Multi Modal Logic into Predicate Logic | 253 |
Default Reasoning with a Constraint Resolution Principle | 265 |
NonClausal Deductive Techniques for Computing Prime Implicants and Prime Implicates | 277 |
Unification in OrderSorted Logic With Term Declarations | 301 |
A System Based on the Inference of Type Relations | 309 |
Parsing with DCGterms | 98 |
A First Order Resolution Calculus with Symmetries | 110 |
Ordered Paramodulation and Resolution as Decision Procedure | 122 |
Static Analysis of Prolog with Cut | 134 |
A New Type Theory for Representing Logics | 146 |
Verification of SwitchLevel Designs with ManyValued Logic | 158 |
Deciding in HFSTheory via Linear Integer Programming | 170 |
The Completion of Typed Logic Programs and SLDNFResolution | 182 |
Increasing the Versatility of Heuristic Based Theorem Provers | 194 |
Sequentialization of Parallel Logic Programs with Mode Analysis | 205 |
A Comparison of Mechanisms for Avoiding Repetition of Subdeductions in Chain Format Linear Deduction Systems | 321 |
Neutralization and Preemption in Extended Logic Programs | 333 |
A System for Axiomatizing Manyvalued Logics | 345 |
A System for Programming with Proofs | 348 |
the marriage of HOL and Maple | 351 |
System Description of LAMBDALG A Higher Order Algebraic Specification Language | 354 |
Mixing metafor | 357 |
A Complete Axiom System for Isomorphism of Types in Closed Categories | 360 |
Reasoning Modeling and ComponentBased Technology | 372 |
Other editions - View all
Logic Programming and Automated Reasoning: 4th International Conference LPAR ... No preview available - 1993 |
Common terms and phrases
Abstract algebra algorithm application approach associated atoms axioms bounded C-literal called clause closed complete computation condition conjunction connection consequence consider consists constant constraint construction contains corresponding deduction default defined definition denote derivation described domain elimination empty equality equations equivalent example exists expression extended factorization finite formula function given goal graph ground holds implementation implicants inference instance interpretation introduced label language Lemma linear literals Logic Programming means mechanism method modal nodes normal Note obtained occurring operation path performed position possible predicate presented problem procedure produces Prolog proof properties propositional prove quantification reasoning relation replace represented resolution respect restricted result rules satisfiable semantics sequence solution sort specification step strategy structure symbols techniques term theorem theory tion transformation transition translation tree unifiable unification University values variables
Bibliographic information
| Title | Logic Programming and Automated Reasoning: 4th International Conference, LPAR'93, St.Petersburg, Russia, July 13-20, 1993. Proceedings Volume 698 of Lecture Notes in Artificial Intelligence, ISSN 0302-9743 Volume 698 of Lecture Notes in Computer Science, ISSN 0302-9743 Volume 698 of Lecture notes in artificial intelligence : Subseries of lecture notes in computer science Volume 698 of Lecture notes in computer science: Lecture notes in artificial intelligence, ISSN 0302-9743 |
| Author | Andrei Voronkov |
| Editor | Andrei Voronkov |
| Edition | illustrated |
| Publisher | Springer Science & Business Media, 1993 |
| ISBN | 3540569448, 9783540569442 |
| Length | 386 pages |
| Subjects | › › Computers / Artificial Intelligence / General Computers / Information Technology Computers / Programming / General Computers / Software Development & Engineering / General Mathematics / Discrete Mathematics Mathematics / History & Philosophy Mathematics / Logic |
| Export Citation | BiBTeX EndNote RefMan |