NDLI: A strong problem reduction method based on function introduction

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

A strong problem reduction method based on function introduction

Content Provider	ACM Digital Library
Author	Baaz, M. Leitsh, A.
Abstract	Although problem reduction is a very important tool in mathematical practice, relatively little attention has been paid to problem reduction in automated theorem proving. A systematical treatment of different problem reduction methods can be found in [BI71] and [Lo78]. (In [BI71] we find unary and binary reduction rules. In the unary case we reduce a problem E to a problem E', where E is provable (refutable) if E' is; for binary reduction we have to produce problems E1, E2 out of E such that E is provable (refutable) if both E1, E2 are provable (refutable).)In finding stronger reduction strategies, one has to give up completeness of the split of E into E1, E2; that means, we only require that the provability of E1 and E2 implies that of E.The authors therefore propose problem reduction based on a splitting rule of the form C → C', where C ∼ C1 &ngr; C2, C' ∼ C1 &ngr; C'2, C'2 ∼ C2 {× ← ƒ(y1,…yn)}, {x,y1,…yn} is the set of variables both in C1 and C2 and ƒ is a new function symbol up to this point not occurring in any clause. Note that the Herbrand universe is extended by ƒ and consequently C' is not derivable from C by usual resolution methods! As (∀y1) … (∀yn(∀x) (C1 &ngr; C2) → (∀y1) … (∀yn ((∀x) C1 &ngr; (∃x) (C2) is valid in first order predicate logic and C1 &ngr; C'2 is the Skolemization of the implied formula, splitting of this kind is correct. For reasons of efficiency (reduction of search space and restriction of compound terms) the authors restrict the application of the rule above to sequences of applications (called Q-reduction) completely separating the variables in C1 and C2.Finally the authors construct a sequence of clause sets Cn having resolution proofs exponential in n only, but application of the new reduction rule reduces the problem to two problems linear in n. Thus it turns out that the introduction of (elementary) quantificational rules into clause logic can strongly influence the structure of proofs and the performance of theorem provers.
Starting Page	30
Ending Page	37
Page Count	8
File Format	PDF
ISBN	0201548925
DOI	10.1145/96877.96888
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