Topological Model Set Deformations in Logic Programming

1989 ◽  
Vol 12 (3) ◽  
pp. 357-399
Author(s):  
Aida Batarekh ◽  
V.S. Subrahmanian
Keyword(s):  
Logic Programming ◽  
Sufficient Conditions ◽  
Topological Spaces ◽  
Logic Programs ◽  
First Order ◽  
Order Language ◽  
Language L ◽  
General Logic ◽  
Model Set ◽  
Necessary And Sufficient

Given a first order language L, and a notion of a logic L w.r.t. L, we investigate the topological properties of the space of L-structures for L. We show that under a topology called the query topology which arises naturally in logic programming, the space of L-models (where L is a decent logic) of any sentence (set of clauses) in L may be regarded as a (closed, compact) T4-space. We then investigate the properties of maps from structures to structures. Our results allow us to apply various well-known results on the fixed-points of operators on topological spaces to the semantics of logic programming – in particular, we are able to derive necessary and sufficient topological conditions for the completion of covered general logic programs to be consistent. Moreover, we derive sufficient conditions guaranteeing the consistency of program completions, and for logic programs to be determinate. We also apply our results to characterize consistency of the unions of program completions.

scholarly journals Decidability of the Clark's completion semantics for monadic programs and queries

2014 ◽  
Vol 15 (3) ◽  
pp. 402-412
Author(s):  
LEVON HAYKAZYAN
Keyword(s):  
Logic Programming ◽  
Logic Programs ◽  
First Order ◽  
Order Language ◽  
General Logic ◽  
Turing Complete

AbstractThere are many different semantics for general logic programs (i.e. programs that use negation in the bodies of clauses). Most of these semantics are Turing complete (in a sense that can be made precise), implying that they are undecidable. To obtain decidability one needs to put additional restrictions on programs and queries. In logic programming it is natural to put restrictions on the underlying first-order language. In this note, we show the decidability of the Clark's completion semantics for monadic general programs and queries.

Algebraic Foundations of Logic Programming, I: The Distributive Lattice of Logic Programs

1990 ◽  
Vol 13 (3) ◽  
pp. 317-332
Author(s):  
Anil Hirani ◽  
V.S. Subrahmanian
Keyword(s):  
Distributive Lattice ◽  
Logic Program ◽  
Logic Programs ◽  
Intended Meaning ◽  
Zero Divisors ◽  
Order Language ◽  
Language L ◽  
General Logic ◽  
Pure Logic ◽  
Algebraic Properties

Given a logic program P, the operator TP associated with P is closely related to the intended meaning of P. Given a first order language L that is generated by finitely many non-logical symbols, our aim is to study the algebraic properties of the set {TP|P is a general logic program in language L} with certain operators on it. For the operators defined in this paper the resulting algebraic structure is a bounded distributive lattice. Our study extends (to the case of general logic programs), the work of Mancarella and Pedreschi who initiated a study of the algebraic properties of the space of pure logic programs. We study the algebraic properties of this set and identify the ideals and zero divisors. In addition, we prove that our algebra satisfies various non-extensibility conditions.

Resolution systems and their applications I

1980 ◽  
Vol 3 (2) ◽  
pp. 235-268
Author(s):  
Ewa Orłowska
Keyword(s):  
Theorem Proving ◽  
Sufficient Conditions ◽  
Predicate Calculus ◽  
Resolution Method ◽  
First Order ◽  
Deductive Systems ◽  
Resolution System ◽  
Resolution Principle ◽  
Necessary And Sufficient ◽  
Classical Predicate

The central method employed today for theorem-proving is the resolution method introduced by J. A. Robinson in 1965 for the classical predicate calculus. Since then many improvements of the resolution method have been made. On the other hand, treatment of automated theorem-proving techniques for non-classical logics has been started, in connection with applications of these logics in computer science. In this paper a generalization of a notion of the resolution principle is introduced and discussed. A certain class of first order logics is considered and deductive systems of these logics with a resolution principle as an inference rule are investigated. The necessary and sufficient conditions for the so-called resolution completeness of such systems are given. A generalized Herbrand property for a logic is defined and its connections with the resolution-completeness are presented. A class of binary resolution systems is investigated and a kind of a normal form for derivations in such systems is given. On the ground of the methods developed the resolution system for the classical predicate calculus is described and the resolution systems for some non-classical logics are outlined. A method of program synthesis based on the resolution system for the classical predicate calculus is presented. A notion of a resolution-interpretability of a logic L in another logic L ′ is introduced. The method of resolution-interpretability consists in establishing a relation between formulas of the logic L and some sets of formulas of the logic L ′ with the intention of using the resolution system for L ′ to prove theorems of L. It is shown how the method of resolution-interpretability can be used to prove decidability of sets of unsatisfiable formulas of a given logic.

System Properties of One-Dimensional Distributed Systems

1977 ◽  
Vol 99 (2) ◽  
pp. 85-90 ◽  
Author(s):  
L. S. Bonderson
Keyword(s):  
Distributed Systems ◽  
Sufficient Conditions ◽  
State Variables ◽  
One Dimensional ◽  
First Order ◽  
Lumped Element ◽  
Order Form ◽  
Power Product ◽  
System Properties ◽  
Necessary And Sufficient

The system properties of passivity, losslessness, and reciprocity are defined and their necessary and sufficient conditions are derived for a class of linear one-dimensional multipower distributed systems. The utilization of power product pairs as state variables and the representation of the dynamics in first-order form allows results completely analogous to those for lumped-element systems.

ORDER AND CONVERGENCE OF THE ENHANCED 3-POINT FULLY IMPLICIT SUPER CLASS OF BLOCK BACKWARD DIFFERENTIATION FORMULA FOR SOLVING INITIAL VALUE PROBLEM

2021 ◽  
Vol 5 (2) ◽  
pp. 442-446
Author(s):  
Muhammad Abdullahi ◽  
Hamisu Musa
Keyword(s):  
Initial Value Problem ◽  
Initial Value Problems ◽  
Sufficient Conditions ◽  
Initial Value ◽  
Differentiation Formula ◽  
Stiff Initial Value Problems ◽  
First Order ◽  
Backward Differentiation Formula ◽  
Fully Implicit ◽  
Necessary And Sufficient

This paper studied an enhanced 3-point fully implicit super class of block backward differentiation formula for solving stiff initial value problems developed by Abdullahi & Musa and go further to established the necessary and sufficient conditions for the convergence of the method. The method is zero stable, A-stable and it is of order 5. The method is found to be suitable for solving first order stiff initial value problems

Necessary and sufficient conditions for oscillation of nonlinear first-order forced differential equations with several delays of neutral type

Analysis ◽  
2019 ◽  
Vol 39 (3) ◽  
pp. 97-105 ◽  
Author(s):  
Sandra Pinelas ◽  
Shyam S. Santra
Keyword(s):  
Differential Equations ◽  
Neutral Type ◽  
Sufficient Conditions ◽  
Necessary And Sufficient Conditions ◽  
First Order ◽  
Several Delays ◽  
Necessary And Sufficient ◽  
T Tau ◽  
First Order Differential Equations

AbstractIn this work, necessary and sufficient conditions are obtained such that every solution of nonlinear neutral first-order differential equations with several delays of the form\bigl{(}x(t)+r(t)x(t-\tau)\bigr{)}^{\prime}+\sum_{i=1}^{m}\phi_{i}(t)H\bigl{(}% x(t-\sigma_{i})\bigr{)}=f(t)is oscillatory or tends to zero as {t\rightarrow\infty.} This problem is considered in various ranges of the neutral coefficient r. Finally, some illustrating examples are presented to show that feasibility and effectiveness of main results.

scholarly journals Oscillatory and Asymptotic Behavior of a First-Order Neutral Equation of Discrete Type with Variable Several Delay under Δ Sign

2018 ◽  
Vol 2018 ◽  
pp. 1-8
Author(s):  
Radhanath Rath ◽  
Chittaranjan Behera
Keyword(s):  
Difference Operator ◽  
Sufficient Conditions ◽  
Neutral Equation ◽  
Delay Difference Equation ◽  
Neutral Delay ◽  
First Order ◽  
Forward Difference ◽  
Necessary And Sufficient ◽  
Positive Integers ◽  
Delay Difference

We obtain necessary and sufficient conditions so that every solution of neutral delay difference equation Δyn-∑j=1kpnjyn-mj+qnG(yσ(n))=fn oscillates or tends to zero as n→∞, where {qn} and {fn} are real sequences and G∈C(R,R), xG(x)>0, and m1,m2,…,mk are positive integers. Here Δ is the forward difference operator given by Δxn=xn+1-xn, and {σn} is an increasing unbounded sequences with σn≤n. This paper complements, improves, and generalizes some past and recent results.

Sign in / Sign up

Export Citation Format

Share Document