Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 7 of 7
Full-Text Articles in Physical Sciences and Mathematics
A Variable-Free Logic For Mass Terms, William C. Purdy
A Variable-Free Logic For Mass Terms, William C. Purdy
Electrical Engineering and Computer Science - Technical Reports
This paper presents a logic appropriate for mass terms, that is, a logic that does not presuppose interpretation in discrete models. Models may range from atomistic to atomless. This logic is a generalization of the author's work on natural language reasoning. The following claims are made for this logic. First, absence of variables makes it simpler than more conventional formalizations based on predicate logic. Second, capability to deal effectively with discrete terms, and in particular with singular terms, can be added to the logic, making it possible to reason about discrete entities and mass entities in a uniform manner. Third, …
Unification In Modal Theorem Proving, Xiaolin Zhang, Chilukuri K. Mohan
Unification In Modal Theorem Proving, Xiaolin Zhang, Chilukuri K. Mohan
Electrical Engineering and Computer Science - Technical Reports
Modal formulas can be proved by translating them into a three-typed logic and then using unification and resolution, with axioms describing properties of the reachability relation among possible worlds. In this paper, we improve on the algorithms in [1], showing that "strong skolemisation" and occurrence checks are not needed for proving theorems of Q, T, Q4, and S4. We also extend the 'path logic' approach to S5, give the appropriate unification algorithm, and prove its correctness.
Domains For Logic Programming, I. Filippenko, F. L. Morris
Domains For Logic Programming, I. Filippenko, F. L. Morris
Electrical Engineering and Computer Science - Technical Reports
We construct Scott domains well suited to use in an abstract implementation of logic programming, and perhaps to the modelling of other first-order data structures. The domain elements, which we call ‘grafts’, are in effect a sort of directed graphs. The approximation order in the domains corresponds to the relation between tuples of terms, “has a substitution instance”; the price to be paid is that one equivalence class of (tuples of) terms under renaming of variables is represented by many grafts. Graft domains come in two flavors—plain and ‘acyclic’—for modelling on an equal footing logic programming without and with the …
A Proof Procedure For Quantifier-Free Non-Clausal First Order Logic, Neil V. Murray
A Proof Procedure For Quantifier-Free Non-Clausal First Order Logic, Neil V. Murray
Electrical Engineering and Computer Science - Technical Reports
A proof procedure is described which operates on formulas of the predicate calculus which are quantifier-free. The procedure, which involves a single inference rule called NC-resolution, is shown to be complete. Completeness is also obtained for a simple restriction on the rule’s application. Examples are given using NC-resolution not only for synthesis of a logic program from its specification, but for execution of a program specification in its original form.
Dual-Mode Sequential Logic For Function Independent Fault-Testing, Sumit Dasgupta, Carlos R.P. Hartmann, Luther D. Rudolph
Dual-Mode Sequential Logic For Function Independent Fault-Testing, Sumit Dasgupta, Carlos R.P. Hartmann, Luther D. Rudolph
Electrical Engineering and Computer Science - Technical Reports
This paper presents a method of using hardware redundancy to ease the problem of fault testing in sequential logic networks. Sequential logic networks are constructed using two kinds of dual-mode logic gates, one of which is specifically required to initialize a feedback loop to some logic value. Initially, it is shown that these networks can be tested for all single stuck-at-faults with six function-independent tests. Next, this method is generalized to detect large classes of multiple faults with six function-independent tests. In both cases, the network must have the proper number of extra inputs.
Dual-Mode Combinational Logic For Function-Independent Fault Testing, Sumit Dasgupta
Dual-Mode Combinational Logic For Function-Independent Fault Testing, Sumit Dasgupta
Electrical Engineering and Computer Science - Technical Reports
This paper presents a method of using hardware redundancy to ease the problem of fault testing in combinational logic networks. Combinational logic networks are constructed using dual-mode logic gates. Initially, it is shown that these networks can be tested for all single stuck-at-faults using just two function-independent tests. This method is then extended to detect a large class of multiple faults with the same two function-independent tests.
Two Models For Combinatory Logic, Luis E. Sanchis
Two Models For Combinatory Logic, Luis E. Sanchis
Electrical Engineering and Computer Science - Technical Reports
We consider in this paper two models of combinatoric logic in which the domain is the same : P(N) the power set of N = the set of non negative integers.