1. A Multiple-Conclusion Meta-Logic - A Multiple-conclusion Meta-logic,Dale Miller
The theory of cut-free sequent proofs has been used to motivate and justify the design of a number of logic programming languages. Two such languages, Prolog and its linear logic refinement, Lolli [12], provide for various forms of abstraction (modules, abstract data types, higher-order programming) but lack primitives for concurrency. The logic programming language, LO (Linear Objects) [2] provides for concurrency but lacks abstraction mechanisms. In this paper we present Forum, a logic programming presentation of all of linear logic that modularly extends the languages Prolog, Lolli, and LO. Forum, therefore, allows specifications to incorporate both abstractions and concurrency. As a meta-language, Forum greatly extends the expressiveness of these other logic programming languages. To illustrate...

2. A Logic for Object-Z - A Logic For Object-z,Graeme Smith
This paper presents a logic for Object-Z which extends W , the logic for Z adopted as the basis of the deductive system in the Z Base Standard. The logic provides a basis on which tool support for reasoning about Object-Z specifications can be developed. It also formalises the intended meaning of Object-Z constructs and hence provides an abstract, axiomatic semantics of the language. 1 Introduction Object-Z[10, 11, 7] is an extension of Z in which the existing syntax and semantics of Z are retained and new constructs are introduced to facilitate specification in an objectoriented style. The enhanced structuring improves the readability of large specifications. It also enables...

3. A Deterministic Terminating Sequent Calculus for Gödel-Dummett logic - Godel-dummett Logic
We give a short proof-theoretic treatment of a terminating contraction-free calculus G4-LC for the zero-order Godel-Dummett logic LC. This calculus is a slight variant of a calculus given by Avellone et al, who show its completeness by model-theoretic techniques. In our calculus, all the rules of G4-LC are invertible, thus allowing a deterministic proof-search procedure. Keywords: sequent calculus, contraction-free, terminating, Godel-Dummett logic 1 Introduction In previous work [9] the author gave a "contraction-free calculus" for zero-order intuitionistic logic IPL; following [21] we call this calculus G4ip. It has the property that root-first proof search terminates, thus allowing easy implementation without a loop-checker. See [9] for further history of this...

4. Free Variables and Subexpressions in Higher-Order Meta Logic - Meta Logic,Chuck Liang
This paper addresses the problem of how to represent free variables and subexpressions involving -bindings. The aim is to apply what is known as higher-order abstract syntax to higher-order term rewriting systems. Directly applying fi-reduction for the purpose of subtermreplacement is incompatible with the requirements of term-rewriting. A new meta-level representation of subterms is developed that will allow term-rewriting systems to be formulated in a higher-order meta logic.

5. Addendum to the paper "Belnap's four-valued logic and De Morgan lattices" - Four-valued Logic,De Morgan
the three above mentioned Gentzen systems are presented, together with the structural and multiple-conclusion versions and of GB and GBL , respectively. Then Theorem 4.88 of [7] states the same as Theorem 4.11 of [3], that is, the strong algebraizability of GB (denoted by in [7]), with the variety DM of De Morgan lattices as its equivalent algebraic semantics. And Theorem 4.98 of [7] states the non-algebraizability of , which is proved from the strong algebraizability of ; since it is obvious that the same fact and proof hold for their single-conclusion fragments, one can consider that this result also contains the non-algebraizability of GBL , which is the assertion in Theorem...

6. Two paradigms of logical computation in Affine Logic? - Affine Logic,G. Bellin,A Silvia Baraldini
We propose a notion of symmetric reduction for a system of proofnets for Multiplicative Affine Logic (MAL + MIX) (namely, multiplicative linear logic with unrestricted Weakening and Mix), related to the "cross-cut" reduction in classical logic LK. We prove that such a reduction has the strong normalization and the Church-Rosser properties. On one hand, the usual asymmetric cut elimination procedure in intuitionistic and linear logic is a form of "computation with garbage collection", and the cancellation of irrelevant parts is uniquely determined at any point of the process; such a paradigm can be applied to classical and affine logic through any one of the several known translations of classical logic...

7. Temporalizing Epistemic Default Logic - Temporalizing Epistemic,Default Logic,Temporalizing Epistemic Default,John-jules Meyer B
this paper in the Sections 2 to 6 the logic EDL is presented. As compared with earlier publications ([MH9 l a, MH92a, MH93a,b]), the logic is slightly extended in order to cater for downward reflection in subsequent sections. In Section 7 we define a labeled branching time temporalization of this logic, in spirit of the approach of [FG92]. In Section 8 we define sceptical and credulous entailment relations based on temporal models

8. Verifying Probabilistic Programs Using A Hoare Like Logic - A Hoare Like Logic,J. I. Den Hartog,E. P. De Vink
Probability, be it inherent or explicitly introduced, has become an important issue in the verification of programs. In this paper we study a formalism which allows reasoning about programs which can act probabilistically. To describe probabilistic programs, a basic programming language with an operator for probabilistic choice is introduced and a denotational semantics is given for this language. To specify properties of probabilistic programs, standard first order logic predicates are insufficient, so a notion of probabilistic predicates is introduced. A Hoare-style proof system to check properties of probabilistic programs is given. The proof system for a sublanguage is shown to...

9. Higher-Order Equational Logic - Christian Prehofer,Tu Munchen,Contributions From Tobias Nipkow,C. Prehofer,Higher-order Equational Logic
Syntax" [Pfenning&Elliot 88] Applications: Programming languages, mathematics, formal systems ffl Higher-order theorem proving ffl Declarative Programming C. Prehofer, 6/97 Higher-Order Equational Logic 4 Declarative Programming Paradigms ? XXXXXXXXX Xz XXXXXXXXX Xz 9 9 ? Logic Programming Functional Programming Narrowing Higher-Order LP Higher-Order FP Higher-Order Narrowing C. Prehofer, 6/97 Higher-Order Equational Logic 5 Notation and Basic Definitions Variable Conventions ffl F; G; H;X;Y free variables ffl a; b; c; f; g (function) constants ffl x; y; z bound variables ffl ff; fi type variables ffl u,v,w constants or bound variables -terms: t = F j x j c j x:t j (t 1 t 2 ) Note: x n :s = x 1 : : : x n :s a(s n ) = ((Delta Delta Delta (a s 1 )...

10. Reasoning About Set Constraints Applied to Tractable Inference in Intuitionistic Logic - Intuitionistic Logic,Thomas Drakengren,Peter Jonsson
Automated reasoning about sets has received a considerable amount of interest in the literature. Techniques for such reasoning have been used in, for instance, analyses of programming languages, terminological logics and spatial reasoning. In this paper, we identify a new class of set constraints where checking satisfiability is tractable (i.e. polynomial-time). We show how to use this tractability result for constructing a new tractable fragment of intuitionistic logic. Furthermore, we prove NP-completeness of several other cases of reasoning about sets. 215 1 Introduction There has been considerable interest in formalisms for describing and reasoning about sets. We begin by describing some of these. The most well-studied class of set constraints is, probably,...

11. Concepción de la polivalencia lógica en la Escuela de Varsovia - Domínguez Prieto, Pablo
Lukasiewilz -destacado miembro de la escuela de Luovvarsovia es considerado el fundador de la lógica polivalente. Se analiza en este trabajo la relación existente entre la doctrina de este lógico polaco con la de otros miembros de su misma escuela: Twardowski (fundador de ella y maestro de Lukasiervilz), Kotarbinski, Asdukiewierz Lesmienski (compañeros suyos. Y por último, Jaskowski y Zawirski (miembros de la segunda generación de la escuela de Luovvarsovia). En todos ellos, si bien no abundan doctrinas explícitas acerca de la polivalencia lógica, si son tratadas cuestiones de lógica, de filosofía del lenguaje o de filosofía de la ciencia fronteriza...

12. La (lógica) contrucción de la realidad - Carrillo Guerrero, Lázaro
Every language activity requires some cognitive representations and some logic constructions in order to function upon the world and to get a position in the face of what is necessarily or probably truthful. In linguistic communication, this makes that the text be built according to some concrete and social logic alternatives, and that within each discourse there have an erected reality that is adaptable to the interlocutors and to the situations, and variable according to the participants' capacity and their strategic conjectures. In this frame, of social interaction and of language-thought relation, it is spread out an argumentative logic that...

13. F-logic Semantics and Implementation of Internet Metadata - Technische Universitaet Dresden,Computational Logic
this document as a customer order and can then locate all properties in an accurate way, since in the document they are showed with tags explicitly.

14. A LOGIC PROGRAMMING EXTENSION FOR C CALLED CLOG - MARIA DO CARMO ELIAS ALVES
The use of declarative languages based in logic programming has been spread out due to the great interest in Artificial Intelligence. However, the use of these languages is not evident yet due to performance, portability, integration to other languages capability and other restrictions. This work contains the definition and implementation of a logic programming extension for C called Clog, which intends to cover the above deficiencies, allowing, mainly, the implementation of applications that have logic programming characteristics integrated to interative programming in the same development environment.

15. Metric similarities in the logic of approximation. - Katz, Michael
We describe restricted and extended versions of the logic of approximation which is meant to handle formally the problems of measurement error and of deduction under conditions of uncertainty. We apply the logic to the foundations of social and behavioral inquiry, axiomatizing in it an inexact similarity predicate which behaves like a metric approximation to identity. In the restricted version of the logic we formulate conditions for the imbeddability of similarity models in the real line, and in the extended version we relate arbitrary predicates of our formal language to the predicate of metric similarity.

16. La lógica como ciencia social y el fenómeno de la modernidad: el caso de Henri Lefebvre - Villanueva Donoso, Jaime
La Lógica constituye un cuerpo fundamentalmente metodológico, con el cual se opera dentro de los distintos ámbitos del saber, por ello han tenido lugar una serie de propuestas formales emplazadas en los distintos ámbitos de las ciencias, la que aquí nos ocupa es el ensayo de una propuesta lógica para el ámbito de las ciencias sociales, pretensión que alcanza en Henri Lefebvre uno de los desarrollos y soluciones de mayor alcance y rigor, más allá de lo puramente formal. Lefebvre, dota así de nuevas perspectivas a la lógica dialéctica, ampliando su alcance, situándola a través su posición crítica frente al...

17. Implementing a prioritized logic programming system : thesis - Wu, Cheng-min
Rule based knowledge representation and reasoning often face a problem of conflict with rules. One common way of solving conflicts is to introduce priorities associate with rules. The thesis describes the underlying algorithm to implement prioritized logic programs (PLPs) proposed by Zhang and Foo in 1997. PLPs are proposed as an extension of Gelfond and Lifschitz's extended logic programs by introducing preferences associatied with rules to the program, where answer sets provide a semantics of PLPs. Major algorithms are presented in detail, and how answer sets can be derived from the algorithm demonstrated. Under this implementation, a PLP is computed...

18. Logica positiva : plenitude, potencialidade e problemas (do pensar sem negação) - Tomas Andres Barrero Guzman
O trabalho estuda o papel da negação na logica, abordando os fragmentos positivos da logica proposicional, de forma a atender a dois problemas: a obtenção de teoremas de completude independentes da negação e o problema de paradoxos positivos, como o Paradoxo de Curry. Para o fragmentoclassico, estuda-se o metodo construtivo de completude proposto por Leon Henkin. Investigam-se as razoes pelas quais este metodo nao pode ser estendido para fragmentos nao-classicos que conseguem evitar a ocorrencia da objeção de Haskel Curry como, por exemplo, os das logicas n-valentes de Jan Lukasiewicz e os (por nos denominados) intuicionistas de Wilhelm Ackermann, quer...

19. Episodes, Characterising Sentences and Causes: A Critique of Episodic Logic - Lenhart K. Schubert's,Chris Fox,Episodic Logic (el
This paper is not intended to undermine this theoretical and applied work. It aims merely to illustrate some problems with the informal intuitions that purport to explain and justify the formal theory of EL. In particular, this paper criticises the view that we should think of events as situations (episodes) which can be completely characterised by natural language sentences. I argue that: (1) there are no genuine natural language examples which require it; (2) it results in a loss of expressiveness; and (3) it leads to problems when giving the logical form of causal statements. I suggest that the motivating example can be dealt with adequately using...

20. Logic Programming in Affine Logic
Traditional logic programming languages, such as Prolog, apply the methods of classical logic to programming tasks. Recently, computer scientists introduced new logic programming languages, based on linear logic rather than classical logic. While classical logic models information that does not change, linear logic models changes of state, and accounts for finite resources, such as money or computer memory, simply and directly. It has been applied to concurrency, natural language processing, updating information in databases, and other resource-sensitive problems. Affine logic is related to linear logic and has a similar range of applications but with a different emphasis. In a linear logic system, axioms mean that a particular...

Página de resultados:
1  2  3  4  5  6  7  8  9  10  Siguiente