NDLI: Equations, disequations and unsolvable subsets (abstract)

Please wait, while we are loading the content...

Normal forms in function fields

A test for λ-confluence for certain prefix rewriting systems with applications to the generalized word problem

PRECOMAS an implementation of constructive matching methodology

A decidable fragment of the elementary theory of relations and some applications

A strong problem reduction method based on function introduction

Resolution proof systems with weak transformation rules

Dataflow for logic program as substitution manipulator

Reexamining intractability of tableau methods

Advances and trends in the design and construction of algebraic manipulation systems

Algebraic programming in the APS system

A delivery system for REDUCE

Univariate power series expansions in REDUCE

SUI: a system independent user interface for an integrated scientific computing environment

Progress report on a system for general-purpose parallel symbolic algebraic computation

How to test in subexponential time whether two points can be connected by a curve in a semialgebraic set

On the isomorphism problem for finite-dimensional binomial algebras

Symbolic solution polynomial equation systems with symmetry

Arithmetic with real algebraic numbers is in NC

On determining the solvability of polynomials

Modular rational sparse multivariate polynomial interpolation

Polynomials over finite fields with large images

Parallel univariate polynomial factorization on shared-memory multiprocessors

Gröbner basis, integration and transcendental functions

Computation of Catalan's constant using Ramanujan's formula

A random base change algorithm for permutation groups

FIDE: a REDUCE package for automation of FInite difference method for solving pDE

Symbolic—numerical computations in the stability analyses of difference schemes

Local approximation study of difference operators by means of REDUCE system

Global theory of ordinary differential equations and formula manipulation

A Critical-pair/completion based integration algorithm

An algorithm of constructing the integral of a module--an infinite dimensional analog of Gröbner basis

The algorithm for calculating integrals of hypergeometric type functions and its realization in REDUCE system

Complexity of irreducibility testing for a system of linear ordinary differential equations

An algorithm for computing the formal solutions of differential systems in the neighborhood of an irregular singular point

On Liouvillian solutions of homogeneous linear differential equations

Reduction problems in the theory of differential equations

Computer generation of necessary integrability conditions for polynomial-nonlinear evolution systems

Automated reasoning in geometries using the characteristic set method and Gröbner basis method

An improvement of the projection operator in cylindrical algebraic decomposition

Methods for mechanical geometry formula deriving

Regular curves and proper parametrizations

Refutational proofs of geometry theorems via characteristic set computation

An algebraic model for the parallel interpretation of equationally defined functions (abstract)

Application of metasystem transition to function inversion and transformation

An execution model for exploiting and-or parallelism in logic programs (abstract)

Equations, disequations and unsolvable subsets (abstract)

A Meta simplifier

Systems for symbolic computations in boolean algebra

Detecting algebraic dependencies between unnested radicals (extended abstract)

Parallel polynomial computations by recursive processes

Solving systems of bivariate algebraic equations by using primitive polynomial remainder sequences

A parallelization of the Buchberger algorithm

On factoring multi-variate polynomials over algebraically closed fields (abstract)

A modular approach to the computation of the number of real roots

Solving algebraic systems which arise as necessary integrability conditions for polynomial-nonlinear evolution equations

An algorithm for finding all isolated zeros of polynomial systems

Application of REDUCE system for analyzing consistency of systems of P.D.E.'s

Some applications of Maple symbolic computation to scientific and engineering problems

On the symbolic/numeric hybrid integration

Optimization techniques for symbolic equation solver in engineering applications

Symbolic and algebraic manipulation for formulae of interpolation and quadrature

The implementation of an algorithm in Macsyma: computing the formal solutions of differential systems in the neighborhood of regular singular point

Equations, disequations and unsolvable subsets (abstract)

Content Provider	ACM Digital Library
Author	Codognet, P.
Abstract	We present a framework for solving a system of equations and disequations that allow to determine, upon unsolvability, the “cause” of the failure, i.e. the minimal unsolvable subsets of equations and disequations responsible of it.Solving equations in the algebra of term is well-known as unification. However if usual unification algorithms are apt to give a unifier when the set is unifiable they don't give any pertinent information when the set in not unifiable. An interesting problem is to determine, in case of unsolvability (minimal) unsolvable subsets cause of the failure of the whole set, i.e. isolate the equations that lead to failure. An immediate application of such an enhanced unification algorithm is in so called intelligent backtracking methods in resolution-based systems, see for instance [Cod 88]. Consider that the set of equations to solve corresponds to the current substitution of a proof method based on the Resolution principle, eg. Logic Programming or most automated theorem provers. Then each equation is associated to a (possible) choice-point in the proof and determining the unsolvable subsets corresponds to isolate pertinent choice-points where it is useful to backtrack to from useless choice-points. This avoids useless deduction/backtracking steps.Recently several authors have been interesting in not only solving sets of equations but also sets of equations and disequations. Colmerauer [Col 84], motivated by the introduction of inequations in Prolog-II, was the first to propose an algorithm to extend his unification algorithm for handling disequations. [Kir 87] presents a set of transformation rules to solve equational problems consisting in a disjunction of conjunctions of equations or disequations with existentially and universally quantified variables. [Com 89] extends this work and gives completness results for transformation rules. This framework clearly separates the control part of the algorithm and encompases a large class of algorithms. As we will restrict ourselves to sets of equations and disequations (i.e. conjunctions), we will use the basic results of [Col 84].Our approach is based on the representation of a set of equations by a unification graph that contain the complete “history” of the unification process, i.e. of variables bindings. This graph represents the solution of the system if it is solvable and allows to easily compute unsolvable subsets (“causes” of the unification failure) in case of failure. This unification graph is formally detailed in [Cod 88], and a simplified version of our algorithm has been implemented as the basis of intelligent backtracking in a Prolog compiler. This system has a low overhead (30%) w.r.t. standard Prolog unification and gives substantial speedups (from 2 to 20) on non-deterministic programs, see once more [Cod 88]. In our approach the unification process consists in the non-deterministic transformation, by two simple derivation rules, of a unification graph corresponding to the initial set of equation to a final irreductible graph corresponding to a solved form. The “cause” of a derived equation can be simply computed by following generalized paths in the graph, and this information is used in case of unsolvability for determining the minimal unsolvable subsets. We then extend our algorithm for dealing with disequations along the lines of [Col 84] and see how unsolvable subsets can also be easily computed thanks to the unification graph for failures due to inequations.See [Cod 90] for a full treatment of our framework.
File Format	PDF
ISBN	0201548925
DOI	10.1145/96877.96956
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1990-07-01
Publisher Place	New York
Access Restriction	Subscribed
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in