text:
doc-src/IsarRef/logics.tex
 author nipkow Wed, 04 Aug 2004 11:25:08 +0200 changeset 15106 e8cef6993701 parent 14682 a5072752114c child 17659 b1019337c857 permissions -rw-r--r--

\chapter{Object-logic specific elements}\label{ch:logics}

\section{General logic setup}\label{sec:object-logic}

\indexisarcmd{judgment}
\indexisarmeth{atomize}\indexisaratt{atomize}
\indexisaratt{rule-format}\indexisaratt{rulify}

\begin{matharray}{rcl}
\isarcmd{judgment} & : & \isartrans{theory}{theory} \\
atomize & : & \isarmeth \\
atomize & : & \isaratt \\
rule_format & : & \isaratt \\
rulify & : & \isaratt \\
\end{matharray}

The very starting point for any Isabelle object-logic is a truth judgment''
that links object-level statements to the meta-logic (with its minimal
language of $prop$ that covers universal quantification $\Forall$ and
implication $\Imp$).

Common object-logics are sufficiently expressive to internalize rule
statements over $\Forall$ and $\Imp$ within their own language.  This is
useful in certain situations where a rule needs to be viewed as an atomic
statement from the meta-level perspective, e.g.\ $\All x x \in A \Imp P(x)$
versus $\forall x \in A. P(x)$.

From the following language elements, only the $atomize$ method and
$rule_format$ attribute are occasionally required by end-users, the rest is
for those who need to setup their own object-logic.  In the latter case
existing formulations of Isabelle/FOL or Isabelle/HOL may be taken as
realistic examples.

Generic tools may refer to the information provided by object-logic
declarations internally.

\railalias{ruleformat}{rule\_format}
\railterm{ruleformat}

\begin{rail}
'judgment' constdecl
;
'atomize' ('(' 'full' ')')?
;
ruleformat ('(' 'noasm' ')')?
;
\end{rail}

\begin{descr}

\item [$\isarkeyword{judgment}~c::\sigma~~(mx)$] declares constant $c$ as the
truth judgment of the current object-logic.  Its type $\sigma$ should
specify a coercion of the category of object-level propositions to $prop$ of
the Pure meta-logic; the mixfix annotation $(mx)$ would typically just link
the object language (internally of syntactic category $logic$) with that of
$prop$.  Only one $\isarkeyword{judgment}$ declaration may be given in any
theory development.

\item [$atomize$] (as a method) rewrites any non-atomic premises of a
sub-goal, using the meta-level equations declared via $atomize$ (as an
attribute) beforehand.  As a result, heavily nested goals become amenable to
fundamental operations such as resolution (cf.\ the $rule$ method) and
proof-by-assumption (cf.\ $assumption$).  Giving the $(full)$'' option
here means to turn the whole subgoal into an object-statement (if possible),
including the outermost parameters and assumptions as well.

A typical collection of $atomize$ rules for a particular object-logic would
provide an internalization for each of the connectives of $\Forall$, $\Imp$,
and $\equiv$.  Meta-level conjunction expressed in the manner of minimal
higher-order logic as $\All{\PROP\,C} (A \Imp B \Imp \PROP\,C) \Imp PROP\,C$
should be covered as well (this is particularly important for locales, see
\S\ref{sec:locale}).

\item [$rule_format$] rewrites a theorem by the equalities declared as
$rulify$ rules in the current object-logic.  By default, the result is fully
normalized, including assumptions and conclusions at any depth.  The
$no_asm$ option restricts the transformation to the conclusion of a rule.

In common object-logics (HOL, FOL, ZF), the effect of $rule_format$ is to
replace (bounded) universal quantification ($\forall$) and implication
($\imp$) by the corresponding rule statements over $\Forall$ and $\Imp$.

\end{descr}

\section{HOL}

\subsection{Primitive types}\label{sec:hol-typedef}

\indexisarcmdof{HOL}{typedecl}\indexisarcmdof{HOL}{typedef}
\begin{matharray}{rcl}
\isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
\isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\
\end{matharray}

\begin{rail}
'typedecl' typespec infix?
;
'typedef' altname? abstype '=' repset
;

altname: '(' (name | 'open' | 'open' name) ')'
;
abstype: typespec infix?
;
repset: term ('morphisms' name name)?
;
\end{rail}

\begin{descr}

\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original
$\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but
also declares type arity $t :: (type, \dots, type) type$, making $t$ an
actual HOL type constructor.

\item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating
non-emptiness of the set $A$.  After finishing the proof, the theory will be
augmented by a Gordon/HOL-style type definition, which establishes a
bijection between the representing set $A$ and the new type $t$.

Technically, $\isarkeyword{typedef}$ defines both a type $t$ and a set (term
constant) of the same name (an alternative base name may be given in
parentheses).  The injection from type to set is called $Rep_t$, its inverse
$Abs_t$ (this may be changed via an explicit $\isarkeyword{morphisms}$
declaration).

Theorems $Rep_t$, $Rep_t_inverse$, and $Abs_t_inverse$ provide the most
basic characterization as a corresponding injection/surjection pair (in both
directions).  Rules $Rep_t_inject$ and $Abs_t_inject$ provide a slightly
more convenient view on the injectivity part, suitable for automated proof
tools (e.g.\ in $simp$ or $iff$ declarations).  Rules
$Rep_t_cases/Rep_t_induct$, and $Abs_t_cases/Abs_t_induct$ provide
alternative views on surjectivity; these are already declared as set or type
rules for the generic $cases$ and $induct$ methods.

An alternative name may be specified in parentheses; the default is to use
$t$ as indicated before.  The $open$ declaration suppresses a separate
constant definition for the representing set.
\end{descr}

Note that raw type declarations are rarely used in practice; the main
application is with experimental (or even axiomatic!) theory fragments.
Instead of primitive HOL type definitions, user-level theories usually refer
to higher-level packages such as $\isarkeyword{record}$ (see
\S\ref{sec:hol-record}) or $\isarkeyword{datatype}$ (see
\S\ref{sec:hol-datatype}).

\indexisarattof{HOL}{split-format}
\begin{matharray}{rcl}
split_format^* & : & \isaratt \\
\end{matharray}

\railalias{splitformat}{split\_format}
\railterm{splitformat}

\begin{rail}
splitformat (((name *) + 'and') | ('(' 'complete' ')'))
;
\end{rail}

\begin{descr}

\item [$split_format~\vec p@1 \dots \vec p@n$] puts expressions of low-level
tuple types into canonical form as specified by the arguments given; $\vec p@i$ refers to occurrences in premise $i$ of the rule.  The $(complete)$''
option causes \emph{all} arguments in function applications to be
represented canonically according to their tuple type structure.

Note that these operations tend to invent funny names for new local
parameters to be introduced.

\end{descr}

\subsection{Records}\label{sec:hol-record}

In principle, records merely generalize the concept of tuples, where
components may be addressed by labels instead of just position.  The logical
infrastructure of records in Isabelle/HOL is slightly more advanced, though,
supporting truly extensible record schemes.  This admits operations that are
polymorphic with respect to record extension, yielding object-oriented''
more details on object-oriented verification and record subtyping in HOL.

\subsubsection{Basic concepts}

Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records at the
level of terms and types.  The notation is as follows:

\begin{center}
\begin{tabular}{l|l|l}
& record terms & record types \\ \hline
fixed & $\record{x = a\fs y = b}$ & $\record{x \ty A\fs y \ty B}$ \\
schematic & $\record{x = a\fs y = b\fs \more = m}$ &
$\record{x \ty A\fs y \ty B\fs \more \ty M}$ \\
\end{tabular}
\end{center}

\noindent The ASCII representation of $\record{x = a}$ is \texttt{(| x = a |)}.

A fixed record $\record{x = a\fs y = b}$ has field $x$ of value $a$ and field
$y$ of value $b$.  The corresponding type is $\record{x \ty A\fs y \ty B}$,
assuming that $a \ty A$ and $b \ty B$.

A record scheme like $\record{x = a\fs y = b\fs \more = m}$ contains fields
$x$ and $y$ as before, but also possibly further fields as indicated by the
$\more$'' notation (which is actually part of the syntax).  The improper
field $\more$'' of a record scheme is called the \emph{more part}.
Logically it is just a free variable, which is occasionally referred to as
row variable'' in the literature.  The more part of a record scheme may be
instantiated by zero or more further components.  For example, the previous
scheme may get instantiated to $\record{x = a\fs y = b\fs z = c\fs \more = m'}$, where $m'$ refers to a different more part.  Fixed records are special
instances of record schemes, where $\more$'' is properly terminated by the
$() :: unit$ element.  Actually, $\record{x = a\fs y = b}$ is just an
abbreviation for $\record{x = a\fs y = b\fs \more = ()}$.

\medskip

Two key observations make extensible records in a simply typed language like
HOL feasible:
\begin{enumerate}
\item the more part is internalized, as a free term or type variable,
\item field names are externalized, they cannot be accessed within the logic
as first-class values.
\end{enumerate}

\medskip

In Isabelle/HOL record types have to be defined explicitly, fixing their field
names and types, and their (optional) parent record.  Afterwards, records may
be formed using above syntax, while obeying the canonical order of fields as
given by their declaration.  The record package provides several standard
operations like selectors and updates.  The common setup for various generic
tutorial \cite{isabelle-hol-book} for further instructions on using records in
practice.

\subsubsection{Record specifications}

\indexisarcmdof{HOL}{record}
\begin{matharray}{rcl}
\isarcmd{record} & : & \isartrans{theory}{theory} \\
\end{matharray}

\begin{rail}
'record' typespec '=' (type '+')? (constdecl +)
;
\end{rail}

\begin{descr}
\item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$]
defines extensible record type $(\vec\alpha)t$, derived from the optional
parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$.

The type variables of $\tau$ and $\vec\sigma$ need to be covered by the
(distinct) parameters $\vec\alpha$.  Type constructor $t$ has to be new,
while $\tau$ needs to specify an instance of an existing record type.  At
least one new field $\vec c$ has to be specified.  Basically, field names
need to belong to a unique record.  This is not a real restriction in
practice, since fields are qualified by the record name internally.

The parent record specification $\tau$ is optional; if omitted $t$ becomes a
root record.  The hierarchy of all records declared within a theory context
forms a forest structure, i.e.\ a set of trees starting with a root record
each.  There is no way to merge multiple parent records!

For convenience, $(\vec\alpha) \, t$ is made a type abbreviation for the
fixed record type $\record{\vec c \ty \vec\sigma}$, likewise is
$(\vec\alpha, \zeta) \, t_scheme$ made an abbreviation for $\record{\vec c \ty \vec\sigma\fs \more \ty \zeta}$.

\end{descr}

\subsubsection{Record operations}

Any record definition of the form presented above produces certain standard
operations.  Selectors and updates are provided for any field, including the
improper one $more$''.  There are also cumulative record constructor
functions.  To simplify the presentation below, we assume for now that
$(\vec\alpha) \, t$ is a root record with fields $\vec c \ty \vec\sigma$.

\medskip \textbf{Selectors} and \textbf{updates} are available for any field
(including $more$''):
\begin{matharray}{lll}
c@i & \ty & \record{\vec c \ty \vec \sigma, \more \ty \zeta} \To \sigma@i \\
c@i_update & \ty & \sigma@i \To \record{\vec c \ty \vec\sigma, \more \ty \zeta} \To
\record{\vec c \ty \vec\sigma, \more \ty \zeta}
\end{matharray}

There is special syntax for application of updates: $r \, \record{x \asn a}$
abbreviates term $x_update \, a \, r$.  Further notation for repeated updates
is also available: $r \, \record{x \asn a} \, \record{y \asn b} \, \record{z \asn c}$ may be written $r \, \record{x \asn a\fs y \asn b\fs z \asn c}$.
Note that because of postfix notation the order of fields shown here is
reverse than in the actual term.  Since repeated updates are just function
applications, fields may be freely permuted in $\record{x \asn a\fs y \asn b\fs z \asn c}$, as far as logical equality is concerned.  Thus
commutativity of independent updates can be proven within the logic for any
two fields, but not as a general theorem.

\medskip The \textbf{make} operation provides a cumulative record constructor
function:
\begin{matharray}{lll}
t{\dtt}make & \ty & \vec\sigma \To \record{\vec c \ty \vec \sigma} \\
\end{matharray}

\medskip We now reconsider the case of non-root records, which are derived of
some parent.  In general, the latter may depend on another parent as well,
resulting in a list of \emph{ancestor records}.  Appending the lists of fields
of all ancestors results in a certain field prefix.  The record package
automatically takes care of this by lifting operations over this context of
ancestor fields.  Assuming that $(\vec\alpha) \, t$ has ancestor fields $\vec b \ty \vec\rho$, the above record operations will get the following types:
\begin{matharray}{lll}
c@i & \ty & \record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty
\zeta} \To \sigma@i \\
c@i_update & \ty & \sigma@i \To
\record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty \zeta} \To
\record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty \zeta} \\
t{\dtt}make & \ty & \vec\rho \To \vec\sigma \To
\record{\vec b \ty \vec\rho, \vec c \ty \vec \sigma} \\
\end{matharray}
\noindent

\medskip Some further operations address the extension aspect of a derived
record scheme specifically: $fields$ produces a record fragment consisting of
exactly the new fields introduced here (the result may serve as a more part
elsewhere); $extend$ takes a fixed record and adds a given more part;
$truncate$ restricts a record scheme to a fixed record.

\begin{matharray}{lll}
t{\dtt}fields & \ty & \vec\sigma \To \record{\vec c \ty \vec \sigma} \\
t{\dtt}extend & \ty & \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma} \To
\zeta \To \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma, \more \ty \zeta} \\
t{\dtt}truncate & \ty & \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma, \more \ty \zeta} \To
\record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma} \\
\end{matharray}

\noindent Note that $t{\dtt}make$ and $t{\dtt}fields$ actually coincide for root records.

\subsubsection{Derived rules and proof tools}

The record package proves several results internally, declaring these facts to
appropriate proof tools.  This enables users to reason about record structures
quite conveniently.  Assume that $t$ is a record type as specified above.

\begin{enumerate}

\item Standard conversions for selectors or updates applied to record
constructor terms are made part of the default Simplifier context; thus
proofs by reduction of basic operations merely require the $simp$ method
without further arguments.  These rules are available as $t{\dtt}simps$,
too.

\item Selectors applied to updated records are automatically reduced by an
internal simplification procedure, which is also part of the standard
Simplifier setup.

\item Inject equations of a form analogous to $((x, y) = (x', y')) \equiv x=x' \conj y=y'$ are declared to the Simplifier and Classical Reasoner as $iff$
rules.  These rules are available as $t{\dtt}iffs$.

\item The introduction rule for record equality analogous to $x~r = x~r' \Imp y~r = y~r' \Imp \dots \Imp r = r'$ is declared to the Simplifier, and as the
basic rule context as $intro?$''.  The rule is called $t{\dtt}equality$.

\item Representations of arbitrary record expressions as canonical constructor
terms are provided both in $cases$ and $induct$ format (cf.\ the generic
proof methods of the same name, \S\ref{sec:cases-induct}).  Several
variations are available, for fixed records, record schemes, more parts etc.

The generic proof methods are sufficiently smart to pick the most sensible
rule according to the type of the indicated record expression: users just
need to apply something like $(cases~r)$'' to a certain proof problem.

\item The derived record operations $t{\dtt}make$, $t{\dtt}fields$,
$t{\dtt}extend$, $t{\dtt}truncate$ are \emph{not} treated automatically, but
usually need to be expanded by hand, using the collective fact
$t{\dtt}defs$.

\end{enumerate}

\subsection{Datatypes}\label{sec:hol-datatype}

\indexisarcmdof{HOL}{datatype}\indexisarcmdof{HOL}{rep-datatype}
\begin{matharray}{rcl}
\isarcmd{datatype} & : & \isartrans{theory}{theory} \\
\isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\
\end{matharray}

\railalias{repdatatype}{rep\_datatype}
\railterm{repdatatype}

\begin{rail}
'datatype' (dtspec + 'and')
;
repdatatype (name *) dtrules
;

dtspec: parname? typespec infix? '=' (cons + '|')
;
cons: name (type *) mixfix?
;
dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
\end{rail}

\begin{descr}
\item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL.
\item [$\isarkeyword{rep_datatype}$] represents existing types as inductive
ones, generating the standard infrastructure of derived concepts (primitive
recursion etc.).
\end{descr}

The induction and exhaustion theorems generated provide case names according
to the constructors involved, while parameters are named after the types (see
also \S\ref{sec:cases-induct}).

See \cite{isabelle-HOL} for more details on datatypes, but beware of the
old-style theory syntax being used there!  Apart from proper proof methods for
case-analysis and induction, there are also emulations of ML tactics
\texttt{case_tac} and \texttt{induct_tac} available, see
\S\ref{sec:hol-induct-tac}; these admit to refer directly to the internal
structure of subgoals (including internally bound parameters).

\subsection{Recursive functions}\label{sec:recursion}

\indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{recdef-tc}
\begin{matharray}{rcl}
\isarcmd{primrec} & : & \isartrans{theory}{theory} \\
\isarcmd{recdef} & : & \isartrans{theory}{theory} \\
\isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\
\end{matharray}

\railalias{recdefsimp}{recdef\_simp}
\railterm{recdefsimp}

\railalias{recdefcong}{recdef\_cong}
\railterm{recdefcong}

\railalias{recdefwf}{recdef\_wf}
\railterm{recdefwf}

\railalias{recdeftc}{recdef\_tc}
\railterm{recdeftc}

\begin{rail}
'primrec' parname? (equation +)
;
'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints?
;
recdeftc thmdecl? tc
;

equation: thmdecl? prop
;
hints: '(' 'hints' (recdefmod *) ')'
;
recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod
;
tc: nameref ('(' nat ')')?
;
\end{rail}

\begin{descr}

\item [$\isarkeyword{primrec}$] defines primitive recursive functions over

\item [$\isarkeyword{recdef}$] defines general well-founded recursive
$(permissive)$'' option tells TFL to recover from failed proof attempts,
returning unfinished results.  The $recdef_simp$, $recdef_cong$, and
$recdef_wf$ hints refer to auxiliary rules to be used in the internal
automated proof process of TFL.  Additional $clasimpmod$ declarations (cf.\
\S\ref{sec:clasimp}) may be given to tune the context of the Simplifier
(cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\
\S\ref{sec:classical}).

\item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover
termination condition number $i$ (default $1$) as generated by a
$\isarkeyword{recdef}$ definition of constant $c$.

Note that in most cases, $\isarkeyword{recdef}$ is able to finish its
internal proofs without manual intervention.

\end{descr}

Both kinds of recursive definitions accommodate reasoning by induction (cf.\
\S\ref{sec:cases-induct}): rule $c\mathord{.}induct$ (where $c$ is the name of
the function definition) refers to a specific induction rule, with parameters
named according to the user-specified equations.  Case names of
$\isarkeyword{primrec}$ are that of the datatypes involved, while those of
$\isarkeyword{recdef}$ are numbered (starting from $1$).

The equations provided by these packages may be referred later as theorem list
$f{\dtt}simps$, where $f$ is the (collective) name of the functions defined.
Individual equations may be named explicitly as well; note that for
$\isarkeyword{recdef}$ each specification given by the user may result in
several theorems.

\medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using
the following attributes.

\indexisarattof{HOL}{recdef-simp}\indexisarattof{HOL}{recdef-cong}\indexisarattof{HOL}{recdef-wf}
\begin{matharray}{rcl}
recdef_simp & : & \isaratt \\
recdef_cong & : & \isaratt \\
recdef_wf & : & \isaratt \\
\end{matharray}

\railalias{recdefsimp}{recdef\_simp}
\railterm{recdefsimp}

\railalias{recdefcong}{recdef\_cong}
\railterm{recdefcong}

\railalias{recdefwf}{recdef\_wf}
\railterm{recdefwf}

\begin{rail}
(recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del')
;
\end{rail}

\subsection{Definition by specification}\label{sec:hol-specification}

\indexisarcmdof{HOL}{specification}
\begin{matharray}{rcl}
\isarcmd{specification} & : & \isartrans{theory}{proof(prove)} \\
\isarcmd{ax_specification} & : & \isartrans{theory}{proof(prove)} \\
\end{matharray}

\begin{rail}
('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
;
decl: ((name ':')? term '(' 'overloaded' ')'?)
\end{rail}

\begin{descr}
\item [$\isarkeyword{specification}~decls~\phi$] sets up a goal stating
the existence of terms with the properties specified to hold for the
constants given in $\mathit{decls}$.  After finishing the proof, the
theory will be augmented with definitions for the given constants,
as well as with theorems stating the properties for these constants.
\item [$\isarkeyword{ax_specification}~decls~\phi$] sets up a goal stating
the existence of terms with the properties specified to hold for the
constants given in $\mathit{decls}$.  After finishing the proof, the
theory will be augmented with axioms expressing the properties given
in the first place.
\item[$decl$] declares a constant to be defined by the specification
given.  The definition for the constant $c$ is bound to the name
$c$\_def unless a theorem name is given in the declaration.
Overloaded constants should be declared as such.
\end{descr}

Whether to use $\isarkeyword{specification}$ or $\isarkeyword{ax_specification}$
is to some extent a matter of style.  $\isarkeyword{specification}$ introduces no new axioms,
and so by construction cannot introduce inconsistencies, whereas $\isarkeyword{ax_specification}$
does introduce axioms, but only after the user has explicitly proven it to be
safe.  A practical issue must be considered, though: After introducing two constants
with the same properties using $\isarkeyword{specification}$, one can prove
that the two constants are, in fact, equal.  If this might be a problem,
one should use $\isarkeyword{ax_specification}$.

\subsection{(Co)Inductive sets}\label{sec:hol-inductive}

\indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{coinductive}\indexisarattof{HOL}{mono}
\begin{matharray}{rcl}
\isarcmd{inductive} & : & \isartrans{theory}{theory} \\
\isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
mono & : & \isaratt \\
\end{matharray}

\begin{rail}
('inductive' | 'coinductive') sets intros monos?
;
'mono' (() | 'add' | 'del')
;

sets: (term +)
;
intros: 'intros' (thmdecl? prop +)
;
monos: 'monos' thmrefs
;
\end{rail}

\begin{descr}
\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
(co)inductive sets from the given introduction rules.
\item [$mono$] declares monotonicity rules.  These rule are involved in the
automated monotonicity proof of $\isarkeyword{inductive}$.
\end{descr}

See \cite{isabelle-HOL} for further information on inductive definitions in
HOL, but note that this covers the old-style theory format.

\subsection{Arithmetic proof support}

\indexisarmethof{HOL}{arith}\indexisarattof{HOL}{arith-split}
\begin{matharray}{rcl}
arith & : & \isarmeth \\
arith_split & : & \isaratt \\
\end{matharray}

\begin{rail}
'arith' '!'?
;
\end{rail}

The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
$real$).  Any current facts are inserted into the goal before running the
procedure.  The !''~argument causes the full context of assumptions to be
included.  The $arith_split$ attribute declares case split rules to be
expanded before the arithmetic procedure is invoked.

Note that a simpler (but faster) version of arithmetic reasoning is already
performed by the Simplifier.

\subsection{Cases and induction: emulating tactic scripts}\label{sec:hol-induct-tac}

The following important tactical tools of Isabelle/HOL have been ported to
Isar.  These should be never used in proper proof texts!

\indexisarmethof{HOL}{case-tac}\indexisarmethof{HOL}{induct-tac}
\indexisarmethof{HOL}{ind-cases}\indexisarcmdof{HOL}{inductive-cases}
\begin{matharray}{rcl}
case_tac^* & : & \isarmeth \\
induct_tac^* & : & \isarmeth \\
ind_cases^* & : & \isarmeth \\
\isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
\end{matharray}

\railalias{casetac}{case\_tac}
\railterm{casetac}

\railalias{inducttac}{induct\_tac}
\railterm{inducttac}

\railalias{indcases}{ind\_cases}
\railterm{indcases}

\railalias{inductivecases}{inductive\_cases}
\railterm{inductivecases}

\begin{rail}
casetac goalspec? term rule?
;
inducttac goalspec? (insts * 'and') rule?
;
indcases (prop +)
;
inductivecases (thmdecl? (prop +) + 'and')
;

rule: ('rule' ':' thmref)
;
\end{rail}

\begin{descr}
\item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes
only (unless an alternative rule is given explicitly).  Furthermore,
$case_tac$ does a classical case split on booleans; $induct_tac$ allows only
variables to be given as instantiation.  These tactic emulations feature
both goal addressing and dynamic instantiation.  Note that named rule cases
are \emph{not} provided as would be by the proper $induct$ and $cases$ proof
methods (see \S\ref{sec:cases-induct}).

\item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface
to the internal \texttt{mk_cases} operation.  Rules are simplified in an
unrestricted forward manner.

While $ind_cases$ is a proof method to apply the result immediately as
elimination rules, $\isarkeyword{inductive_cases}$ provides case split
theorems at the theory level for later use,
\end{descr}

\subsection{Executable code}

Isabelle/Pure provides a generic infrastructure to support code generation
from executable specifications, both functional and relational programs.
Isabelle/HOL instantiates these mechanisms in a way that is amenable to
end-user applications.  See \cite{isabelle-HOL} for further information (this
actually covers the new-style theory format as well).

\indexisarcmd{generate-code}\indexisarcmd{consts-code}\indexisarcmd{types-code}
\indexisaratt{code}

\begin{matharray}{rcl}
\isarcmd{generate_code} & : & \isartrans{theory}{theory} \\
\isarcmd{consts_code} & : & \isartrans{theory}{theory} \\
\isarcmd{types_code} & : & \isartrans{theory}{theory} \\
code & : & \isaratt \\
\end{matharray}

\railalias{generatecode}{generate\_code}
\railterm{generatecode}

\railalias{constscode}{consts\_code}
\railterm{constscode}

\railalias{typescode}{types\_code}
\railterm{typescode}

\begin{rail}
generatecode ( () | '(' name ')') ((name '=' term) +)
;
constscode (name ('::' type)? template +)
;
typescode (name template +)
;
template: '(' string ')'
;

'code' (name)?
;
\end{rail}

\section{HOLCF}

\subsection{Mixfix syntax for continuous operations}

\indexisarcmdof{HOLCF}{consts}

\begin{matharray}{rcl}
\isarcmd{consts} & : & \isartrans{theory}{theory} \\
\end{matharray}

HOLCF provides a separate type for continuous functions $\alpha \to \beta$, with an explicit application operator $f \cdot x$.  Isabelle mixfix
syntax normally refers directly to the pure meta-level function type $\alpha \To \beta$, with application $f\,x$.

The HOLCF variant of $\CONSTS$ modifies that of Pure Isabelle (cf.\
\S\ref{sec:consts}) such that declarations involving continuous function types
are treated specifically.  Any given syntax template is transformed
internally, generating translation rules for the abstract and concrete
representation of continuous application.  Note that mixing of HOLCF and Pure
application is \emph{not} supported!

\subsection{Recursive domains}

\indexisarcmdof{HOLCF}{domain}
\begin{matharray}{rcl}
\isarcmd{domain} & : & \isartrans{theory}{theory} \\
\end{matharray}

\begin{rail}
'domain' parname? (dmspec + 'and')
;

dmspec: typespec '=' (cons + '|')
;
cons: name (type *) mixfix?
;
dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
\end{rail}

Recursive domains in HOLCF are analogous to datatypes in classical HOL (cf.\
\S\ref{sec:hol-datatype}).  Mutual recursion is supported, but no nesting nor
arbitrary branching.  Domain constructors may be strict (default) or lazy, the
latter admits to introduce infinitary objects in the typical LCF manner (e.g.\
domains.

\section{ZF}

\subsection{Type checking}

The ZF logic is essentially untyped, so the concept of type checking'' is
performed as logical reasoning about set-membership statements.  A special
method assists users in this task; a version of this is already declared as a
solver'' in the standard Simplifier setup.

\indexisarcmd{print-tcset}\indexisaratt{typecheck}\indexisaratt{TC}

\begin{matharray}{rcl}
\isarcmd{print_tcset}^* & : & \isarkeep{theory~|~proof} \\
typecheck & : & \isarmeth \\
TC & : & \isaratt \\
\end{matharray}

\begin{rail}
'TC' (() | 'add' | 'del')
;
\end{rail}

\begin{descr}

\item [$\isarcmd{print_tcset}$] prints the collection of typechecking rules of
the current context.

Note that the component built into the Simplifier only knows about those
rules being declared globally in the theory!

\item [$typecheck$] attempts to solve any pending type-checking problems in
subgoals.

\item [$TC$] adds or deletes type-checking rules from the context.

\end{descr}

\subsection{(Co)Inductive sets and datatypes}

\subsubsection{Set definitions}

In ZF everything is a set.  The generic inductive package also provides a
specific view for datatype'' specifications.  Coinductive definitions are
available in both cases, too.

\indexisarcmdof{ZF}{inductive}\indexisarcmdof{ZF}{coinductive}
\indexisarcmdof{ZF}{datatype}\indexisarcmdof{ZF}{codatatype}
\begin{matharray}{rcl}
\isarcmd{inductive} & : & \isartrans{theory}{theory} \\
\isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
\isarcmd{datatype} & : & \isartrans{theory}{theory} \\
\isarcmd{codatatype} & : & \isartrans{theory}{theory} \\
\end{matharray}

\railalias{CONDEFS}{con\_defs}
\railterm{CONDEFS}

\railalias{TYPEINTROS}{type\_intros}
\railterm{TYPEINTROS}

\railalias{TYPEELIMS}{type\_elims}
\railterm{TYPEELIMS}

\begin{rail}
('inductive' | 'coinductive') domains intros hints
;

domains: 'domains' (term + '+') ('<=' | subseteq) term
;
intros: 'intros' (thmdecl? prop +)
;
hints: monos? condefs? typeintros? typeelims?
;
monos: ('monos' thmrefs)?
;
condefs: (CONDEFS thmrefs)?
;
typeintros: (TYPEINTROS thmrefs)?
;
typeelims: (TYPEELIMS thmrefs)?
;
\end{rail}

In the following diagram $monos$, $typeintros$, and $typeelims$ are the same
as above.

\begin{rail}
('datatype' | 'codatatype') domain? (dtspec + 'and') hints
;

domain: ('<=' | subseteq) term
;
dtspec: term '=' (con + '|')
;
con: name ('(' (term ',' +) ')')?
;
hints: monos? typeintros? typeelims?
;
\end{rail}

See \cite{isabelle-ZF} for further information on inductive definitions in
HOL, but note that this covers the old-style theory format.

\subsubsection{Primitive recursive functions}

\indexisarcmdof{ZF}{primrec}
\begin{matharray}{rcl}
\isarcmd{primrec} & : & \isartrans{theory}{theory} \\
\end{matharray}

\begin{rail}
'primrec' (thmdecl? prop +)
;
\end{rail}

\subsubsection{Cases and induction: emulating tactic scripts}

The following important tactical tools of Isabelle/ZF have been ported to
Isar.  These should be never used in proper proof texts!

\indexisarmethof{ZF}{case-tac}\indexisarmethof{ZF}{induct-tac}
\indexisarmethof{ZF}{ind-cases}\indexisarcmdof{ZF}{inductive-cases}
\begin{matharray}{rcl}
case_tac^* & : & \isarmeth \\
induct_tac^* & : & \isarmeth \\
ind_cases^* & : & \isarmeth \\
\isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
\end{matharray}

\begin{rail}
(casetac | inducttac) goalspec? name
;
indcases (prop +)
;
inductivecases (thmdecl? (prop +) + 'and')
;
\end{rail}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "isar-ref"
%%% End:


text:
# Tipping a tetrahedron in a plane

A regular tetrahedron with one black and three white faces is positioned with its black face at the bottom of a plane. The tetrahedron is tipped several times over an edge and finally reaches the same original position.

Is it possible, that the tetrahedron ended up with a white face at the bottom of the plane at its final position?

• While I can see how one arrives at the answer, I'm nowhere near capable of answering this beautifully. +1 Oct 19 at 15:48

It is ...

not Possible.

Proof:

Imagine that the 4 sides have been unrolled to form a Parallelogram.
Let the sides be numbered 1, 2, 3 & 4 which is shown in the Image.
Now all movements in the track along the X axis will repeat in order and this is fixed.
If a movement moves it in the Y axis, it will move up or down into a new track.
Here, again it can move in this track in the X axis which will again be in same order but shifted & reversed.
Moving back to original track will again shift back & reversed back to normal.
Eventually, the Plane will be tiled with the triangles with numbers 1, 2, 3 & 4.

Image:

Conclusion:

No matter which number or which colour is selected to be the black side, it will come back to the Starting Position without change.

• Is there anything preventing me from doing a diagonal flip? If not then starting where you numbered $1$; $1$, $2$, $3$, $4$, $2$ (below), $4$ (back towards $1$), finally landing on $3$ where we started (assuming that $1$ is the black face), unless I confused myself somehow. Oct 19 at 16:51
• I'm pretty sure there is something wrong with your picture. If you keep one corner fixed to the ground and revolve around it you should get six triangles two of each colour except the face opposite the fixed corner. Oct 19 at 16:53
• @loopywalt , good catch , will update shortly ....
– Prem
Oct 19 at 17:35
• @Tacoタコス , My earlier Image was wrong ; I hope it makes sense now. Movements are over edges , not on corners.
– Prem
Oct 19 at 17:44

No, it is not possible.

This is because

all loops have lengths that are a multiple of six, which is a multiple of three, which traps the tetrahedron "T" to only ever have its original position with the black face underneath.

The tetrahedron is composed of four equilateral triangles and "rolling" it fixes one vertex. Continuing to roll it around that vertex will result in a sequence of equilateral triangles all sharing one vertex on the plane. Our basic geometry tells us that six rolls will form a regular hexagon. But any vertex on T is the intersection of exactly three faces, which will cycle in the same order during that roll: * The first and fourth triangles will be made by the first "inside" the white face, * the second and fifth by the second "inside" white face, * the third and sixth (being the last, the same as the original position) by the black face. The "outside" white face never touches the plane during the rolling, because it is not coincident to the vertex which stays on the plane. If we stop and roll backwards on the loop, we are simply returning to the same position, which is pointless. So for T to reach the same position in one loop, it must finish on the same fave it started from. What about multiple loops? Well, they must eventually connect back to one of the three loops that share the original position, and then that loop must be completed or reversed too. Thus, we can never change the face that must land on the original position.

• +1 , Nice Alternative Thought-Process !! While the Conclusion is valid & the reasoning is Partially valid , I think the reasoning is Incomplete : Yes , all loops have length 6 & Paths which go through these Complete loops will come back to Initial Position, .... But there are ways to go around in Partial loops, hop on to other Partial loops, and go in "Arbitrary Directions" , including "Straight lines" and then come back via other routes, all without having Complete loops.
– Prem
Oct 21 at 11:11
• All loops have a length that is a multiple of six. You can never return to a position without making a multiple of six rolls, or retreating back over the path used (which means returning to the original state as well as position). Returning to the original position is the definition of a loop, whether it is formed of straight lines or crazy curves.
– Nij
Oct 21 at 20:05
• You wrote "What about multiple loops? Well, they must connect to one of three loops that share the original position, then that loop must be completed or reversed too." :: (1) With Definition = route is one Big loop, there are no "multiple loops", right ? (2) OK, with the Definition = route is one Big loop, having multiple Small loops, my comment was about Partial Smaller loops being "not completed or reversed". In Starting Small loop, I goto sides 1&2, goto other Partial Small loops, goto Starting Small loop on sides 5&6, goto Starting Position 1 skiping sides 3&4 of Starting Small loop.
– Prem
Oct 22 at 5:39

Imagine coloring the vertex opposite the black face red. As we roll the tetrahedron around, we keep track of the projection of the red vertex onto the plane. It is easy to see that the red vertex will always be constrained to the set of red points below, which form the vertices of a hexagonal grid. In particular, the red vertex will never end up at any of the blue vertices, which is necessary for the tetrahedron to return to the shaded triangle with a different face on bottom.

format: plain


text:
# Prove that $\mathbb{Q}^{\times}$ not isomorphic to $\mathbb{Z}^{n}$

$\mathbb{Q}^{\times}$ is the group of rational number without $0$ under multiplication, and $\mathbb{Z}^{n}$ is the free abelian group of rank $n$. Show that $\mathbb{Q}^{\times}$ not isomorphic to $\mathbb{Z}^{n}$. I tried to assume that there is an isomorphism and to get a contradiction.. didn't succeed

• $\Bbb Q^\times$ has torsion, but free abelian groups do not. In fact $\Bbb Q^\times$ is isomorphic to $\Bbb Z_2\oplus \bigoplus \Bbb Z$ where the sum is over countably many copies of the integers. – Pedro Tamaroff Jan 18 '15 at 16:47
• That's even better, you should put this as an answer, even if it same the same as @Meelo wrote, and as what anyone could wrote. (Bet.) – ujsgeyrr1f0d0d0r0h1h0j0j_juj Jan 18 '15 at 18:17

Suppose you had a homomorphism $f:\mathbb Q^{\times}\rightarrow\mathbb Z^{n}$. Notice that $(-1)^2=1$ thus $f(-1)^2=1$. The only solution to $x^2=e$ (where $e$ is the identity) in $\mathbb Z^{n}$ is $e$, thus $f(-1)=f(1)=e$, meaning no homomorphism is injective and the groups are not isomorphic.

(To be clear, notice that $x^2=e$ in $\mathbb Z^n$ would more commonly be written as $x+x=0$, but I chose to write it multiplicatively to aid seeing the connection between $(-1)^2=1$ (in $\mathbb Q^{\times}$) and $x^2=e$ (in $\mathbb Z^{n}$))

• It is very unorthodox to denote the zero of $\Bbb Z^n$ as $1$. =) – Pedro Tamaroff Jan 18 '15 at 16:50
• I edited its answer properly to address that, but the guy apparently refused my edit... – ujsgeyrr1f0d0d0r0h1h0j0j_juj Jan 18 '15 at 16:52
• @RobertGreen It is better to comment to the poster on such minor detail (which is not incorrect!) rather than to "force" the edit oneself. – Pedro Tamaroff Jan 18 '15 at 16:53
• I would tend to see this as coding with other people. The code does not belong to anyone, and anyone is free to "edit" change it, provided that this edit preserves the function/results etc of the code. Btw, I'm not forcing anything, as he can (and he did) refuse. What I say is that my edit is valid as it corrects what he put in the first place. Instead of validating the edit, he preferred to give an answer that is stil really cumbersome : "$x^2 = e$ in $\mathbf{Z}^n$"... In which serious place have you ever seen this kind of stuff ? ;-) – ujsgeyrr1f0d0d0r0h1h0j0j_juj Jan 18 '15 at 16:56
• @Robert It had not initially occurred to me that the notation $x^2=e$ was at all unnatural and, after seeing your edit, I chose to keep the notation, but to note that it was not standard. I didn't like your edit because it didn't seem helpful to say one group is multiplicative and the other is additive - those properties aren't intrinsic to the group, so I'm unconcerned with them (esp. since I usually think of $\mathbb Z^n\cong \langle a_1,\ldots,a_n | a_ia_j=a_ja_i\rangle$). Your edit was valid, but it conflicted with my intention - a comment (or even separate answer) would have been better. – Milo Brandt Jan 18 '15 at 17:41

$\mathbf{Q}^{\times}$ is generated by the set of positive prime numbers and $-1$ so it contains (a groupe isomorphic to) $\mathbf{Z}^{\mathscr{P}}$ where $\mathscr{P}$ is the set of positive prime numbers. $\mathbf{Z}^{\mathscr{P}}$ is not of finite rank over $\mathbf{Z}$ whereas any $\mathbf{Z}^n$ is, so there's no possible isomorphism $\mathbf{Q}^{\times} \rightarrow \mathbf{Z}^n$, for any $n$, as any such arrow would give an infinite free family in $\mathbf{Z}^n$, namely, the family image of $\mathscr{P}$ by the supposed isomorphism.

To put if in a "fashion" way the morphism $$v : \mathbf{Q}^{\times} \rightarrow \{\pm\}\times \mathbf{Z}^{\mathscr{P}}$$ defined by $v(x) = \left( \textrm{sign}(x), \left( v_p(x)\right)_{p\in \mathscr{P}} \right)$ where $v_p$ is the $p$-adic valuation function for $p\in \mathscr{P}$, is an isomorphism.

This relies on the fact that $\mathscr{P}$ is infinite - fact admitted here. ;-)

• Your argument is that $\mathbf Q^\times_{>0}$ not finitely generated while $\mathbf Z^n$ is. Although this is correct, showing that there is no set of generators of cardinality less than the cardinality of the set of primes (and $-1$) can be unpleasant. – Myself Jan 18 '15 at 16:40
• @Myself Why? It's the fundamental theorem in action; clearly if a given $p_i$ appears in a member of $\mathbb{Q}^\times$ then it has to be in one of the generators... – Steven Stadnicki Jan 18 '15 at 16:47
• Is it really that unpleasant? Any finite set of elements of ${\mathbb Q}^\times$ can only involve finitely many primes in their numerators and denominators, so cannot generate the whole group. – Derek Holt Jan 18 '15 at 16:47
• @Myself forgot to put $-1$, sorry. Nothing is unpleasant actually, as you may see in my edited answer – ujsgeyrr1f0d0d0r0h1h0j0j_juj Jan 18 '15 at 16:48
• Ah maybe it's not quite so unpleasant as I thought :-) For a minute I thought there would be lcm's and gcd's all over the place; but that is for $(\Bbb Q,+)$. – Myself Jan 18 '15 at 16:50


text:
## Nonlinear Analysis. Theory, Methods & Applications

### An International Multidisciplinary Journal

 Short Title: Nonlinear Anal., Theory Methods Appl. Publisher: Elsevier Science Ltd. (Pergamon), Oxford ISSN: 0362-546X Online: http://www.sciencedirect.com/science/journal/0362546X Successor: Nonlinear Analysis. Theory, Methods & Applications. Series A: Theory and MethodsNonlinear Analysis. Real World Applications Comments: No longer indexed
 Documents Indexed: 3,942 Publications (1976–1999) References Indexed: 3,755 Publications with 54,329 References.
all top 5

### Latest Issues

 38, No. 8, A (1999) 38, No. 7, A (1999) 38, No. 6, A (1999) 38, No. 5, B (1999) 38, No. 4, A (1999) 38, No. 3, A (1999) 38, No. 2, A (1999) 38, No. 1, B (1999) 37, No. 8, A (1999) 37, No. 7, A (1999) 37, No. 6, A (1999) 37, No. 5, B (1999) 37, No. 4, A (1999) 37, No. 3, A (1999) 37, No. 2, A (1999) 37, No. 1, B (1999) 36, No. 8, A (1999) 36, No. 7, A (1999) 36, No. 6, B (1999) 36, No. 5, B (1999) 36, No. 4, A (1999) 36, No. 3, A (1999) 36, No. 2, A (1999) 36, No. 1, A (1999) 35, No. 8, B (1999) 35, No. 7, A (1999) 35, No. 6, A (1999) 35, No. 5, A (1999) 35, No. 4, A (1999) 35, No. 3, A (1999) 35, No. 2, A (1999) 35, No. 1, B (1999) 34, No. 7 (1998) 34, No. 6 (1998) 34, No. 5 (1998) 34, No. 4 (1998) 34, No. 3 (1998) 34, No. 2 (1998) 34, No. 1 (1998) 33, No. 7 (1998) 33, No. 6 (1998) 33, No. 5 (1998) 33, No. 4 (1998) 33, No. 3 (1998) 33, No. 2 (1998) 33, No. 1 (1998) 32, No. 7 (1998) 32, No. 6 (1998) 32, No. 5 (1998) 32, No. 4 (1998) 32, No. 3 (1998) 32, No. 2 (1998) 32, No. 1 (1998) 31, No. 7 (1998) 31, No. 5-6 (1998) 31, No. 3-4 (1998) 31, No. 1-2 (1998) 30, No. 8 (1997) 30, No. 7 (1997) 30, No. 6 (1997) 30, No. 5 (1997) 30, No. 4 (1997) 30, No. 3 (1997) 30, No. 2 (1997) 30, No. 1 (1997) 29, No. 12 (1997) 29, No. 11 (1997) 29, No. 10 (1997) 29, No. 9 (1997) 29, No. 8 (1997) 29, No. 7 (1997) 29, No. 6 (1997) 29, No. 5 (1997) 29, No. 4 (1997) 29, No. 3 (1997) 29, No. 2 (1997) 29, No. 1 (1997) 28, No. 12 (1997) 28, No. 11 (1997) 28, No. 10 (1997) 28, No. 9 (1997) 28, No. 8 (1997) 28, No. 7 (1997) 28, No. 6 (1997) 28, No. 5 (1997) 28, No. 4 (1997) 28, No. 3 (1997) 28, No. 2 (1997) 28, No. 1 (1997) 27, No. 12 (1996) 27, No. 11 (1996) 27, No. 10 (1996) 27, No. 9 (1996) 27, No. 8 (1996) 27, No. 7 (1996) 27, No. 6 (1996) 27, No. 5 (1996) 27, No. 4 (1996) 27, No. 3 (1996) 27, No. 2 (1996) ...and 189 more Volumes
all top 5

### Authors

 49 Lakshmikantham, Vangipuram 21 O’Regan, Donal 17 Heikkilä, Seppo V. 16 Altman, Mieczyslaw 15 Bellman, Richard Ernest 15 Kartsatos, Athanassios G. 15 Leela, Srinivasa G. 14 Agarwal, Ravi P. 14 Gupta, Chaitan P. 14 Walter, Wolfgang 14 Yuan, George Xian-Zhi 13 Reich, Simeon 12 Kenmochi, Nobuyuki 12 Lazer, Alan C. 12 Peletier, Lambertus Adrianus 12 Takahashi, Wataru 12 Xu, Hong-Kun 11 Hirano, Norimichi 11 Kaul, Saroop K. 11 Pao, Chia-Ven 11 Petryshyn, Walter Wolodymyr 10 Dancer, Edward Norman 10 Deimling, Klaus 10 Fitzgibbon, William Edward 10 Friedman, Avner 10 Kalaba, Robert E. 10 McKenna, Patrick Joseph 10 Payne, Lawrence Edward 10 Pinto, Manuel 9 Brown, Kenneth J. 9 Carl, Siegfried 9 Hale, Jack Kenneth 9 Krasnosel’skiĭ, Aleksandr Markovich 9 Nakao, Mitsuhiro 9 Solimini, Sergio 9 Tan, Kok-Keong 8 Ahmad, Shair 8 Ahmed, Nasir Uddin 8 Barbu, Viorel 8 Bertsch, Michiel 8 Borwein, Jonathan Michael 8 Feireisl, Eduard 8 Gilbert, Robert Pertsch 8 Abreu Goncalves, Jose Valdo 8 Ledzewicz, Urszula 8 Li, Yong 8 Lions, Pierre-Louis 8 Mawhin, Jean L. 8 Torrejón, Ricardo M. 7 Appell, Jürgen M. 7 Boccardo, Lucio 7 Burton, Theodore Allen 7 Cañada Villar, Antonio 7 Diaz Diaz, Jesus Ildefonso 7 Erbe, Lynn Harry 7 Fečkan, Michal 7 Graef, John R. 7 Guo, Dajun 7 Henderson, Johnny Lee 7 Kannan, Rangachary 7 Kirk, William Arthur 7 Korman, Philip L. 7 Lasiecka, Irena 7 Li, Shujie 7 López-Gómez, Julián 7 Manasevich, Raul F. 7 Miyagaki, Olimpio Hiroshi 7 Nieto Roig, Juan Jose 7 Papageorgiou, Nikolaos S. 7 Park, Sehie 7 Parrott, Mary E. 7 Pavel, Nicolae H. 7 Penot, Jean-Paul 7 Schmitt, Klaus 7 Shivaji, Ratnasingham 7 Swanson, Charles A. 7 Xu, Xiangsheng 7 Zanolin, Fabio 7 Zheng, Songmu 6 Arino, Ovide 6 Berkovits, Juha 6 Cabada, Alberto 6 Castro, Alfonso 6 Chukwu, Ethelbert Nwakuche 6 Da Prato, Giuseppe 6 Ding, Jiu 6 Dinh The Luc 6 Drábek, Pavel 6 Elaydi, Saber Nasr 6 Freedman, Herbert Irving 6 Gossez, Jean-Pierre 6 Guo, Jong-Shenq 6 Hilhorst, Danielle 6 Howes, Frederick A. 6 Hu, Shouchuan 6 Krasnosel’skiĭ, Mark Aleksandrovich 6 Kuang, Yang 6 Lieberman, Gary M. 6 Mustonen, Vesa 6 Myshkis, Anatoliĭ Dmitrievich ...and 3,305 more Authors
all top 5

### Fields

 1,533 Partial differential equations (35-XX) 1,113 Ordinary differential equations (34-XX) 641 Operator theory (47-XX) 401 Calculus of variations and optimal control; optimization (49-XX) 229 Dynamical systems and ergodic theory (37-XX) 221 Biology and other natural sciences (92-XX) 217 Fluid mechanics (76-XX) 201 Global analysis, analysis on manifolds (58-XX) 191 Systems theory; control (93-XX) 182 Numerical analysis (65-XX) 166 Functional analysis (46-XX) 145 Integral equations (45-XX) 119 Mechanics of deformable solids (74-XX) 97 Operations research, mathematical programming (90-XX) 86 General topology (54-XX) 79 Probability theory and stochastic processes (60-XX) 79 Mechanics of particles and systems (70-XX) 67 Real functions (26-XX) 58 Classical thermodynamics, heat transfer (80-XX) 53 Difference and functional equations (39-XX) 46 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 39 Computer science (68-XX) 36 Differential geometry (53-XX) 36 Statistical mechanics, structure of matter (82-XX) 33 Statistics (62-XX) 29 Algebraic topology (55-XX) 25 Measure and integration (28-XX) 18 Geophysics (86-XX) 17 Approximations and expansions (41-XX) 15 Functions of a complex variable (30-XX) 15 Optics, electromagnetic theory (78-XX) 14 Manifolds and cell complexes (57-XX) 14 Quantum theory (81-XX) 10 Relativity and gravitational theory (83-XX) 9 General and overarching topics; collections (00-XX) 7 Linear and multilinear algebra; matrix theory (15-XX) 7 Several complex variables and analytic spaces (32-XX) 7 Information and communication theory, circuits (94-XX) 6 Potential theory (31-XX) 6 Harmonic analysis on Euclidean spaces (42-XX) 6 Convex and discrete geometry (52-XX) 5 Astronomy and astrophysics (85-XX) 4 Nonassociative rings and algebras (17-XX) 4 Integral transforms, operational calculus (44-XX) 3 Number theory (11-XX) 3 Field theory and polynomials (12-XX) 3 Algebraic geometry (14-XX) 3 Topological groups, Lie groups (22-XX) 3 Sequences, series, summability (40-XX) 3 Geometry (51-XX) 2 History and biography (01-XX) 2 Mathematical logic and foundations (03-XX) 2 Combinatorics (05-XX) 2 Category theory; homological algebra (18-XX) 2 Special functions (33-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 Commutative algebra (13-XX) 1 Group theory and generalizations (20-XX)

### Citations contained in zbMATH Open

3,250 Publications have been cited 45,153 times in 33,002 Documents Cited by Year
Inequalities in Banach spaces with applications. Zbl 0757.46033
Xu, Hong-Kun
1991
Boundary regularity for solutions of degenerate elliptic equations. Zbl 0675.35042
Lieberman, Gary M.
1988
$$C^{1+\alpha}$$ local regularity of weak solutions of degenerate elliptic equations. Zbl 0539.35027
DiBenedetto, E.
1983
Abstract critical point theorems and applications to some nonlinear problems with ”strong” resonance at infinity. Zbl 0522.58012
Bartolo, P.; Benci, V.; Fortunato, D.
1983
The Cauchy problem for the critical nonlinear Schrödinger equation in $$H^ s$$. Zbl 0706.35127
Cazenave, Thierry; Weissler, Fred B.
1990
Nonlinear elliptic boundary-value problems in unbounded domains. Zbl 0780.35044
Pao, C. V.
1992
The Choquard equation and related questions. Zbl 0453.47042
Lions, Pierre-Louis
1980
Coupled fixed points of nonlinear operators with applications. Zbl 0635.47045
Guo, Dajun; Lakshmikantham, V.
1987
Nonlinear Schrödinger evolution equations. Zbl 0451.35023
Brézis, Haïm; Gallouet, T.
1980
Some remarks on non local elliptic and parabolic problems. Zbl 0894.35119
Chipot, M.; Lovat, B.
1997
Stabilization of solutions of a degenerate nonlinear diffusion problem. Zbl 0518.35050
Aronson, Donald; Crandall, Michael G.; Peletier, L. A.
1982
Remarks on sublinear elliptic equations. Zbl 0593.35045
Brézis, Haïm; Oswald, Luc
1986
Quasilinear elliptic equations involving critical Sobolev exponents. Zbl 0714.35032
Guedda, Mohammed; Véron, Laurent
1989
Almost everywhere convergence of the gradients of solutions to elliptic and parabolic equations. Zbl 0783.35020
Boccardo, Lucio; Murat, François
1992
A Picone’s identity for the $$p$$-Laplacian and applications. Zbl 0930.35053
Allegretto, Walter; Huang, Yin Xi
1998
A predator-prey model with disease in the prey. Zbl 0922.34036
1999
Nonexpansive iterations in hyperbolic spaces. Zbl 0728.47043
Reich, Simeon; Shafrir, Itai
1990
On the behaviour of measures of noncompactness with respect to differentiation and integration of vector-valued functions. Zbl 0528.47046
Heinz, Hans-Peter
1983
Boundary value problems for nonlinear ordinary differential equations of second order in Banach spaces. Zbl 0462.34041
Mönch, Harald
1980
Convergence of an adaptive penalty scheme for finding constrained equilibria. Zbl 0773.90092
Muu, Le Dung; Oettli, W.
1992
Existence of solutions with prescribed norm for semilinear elliptic equations. Zbl 0877.35091
Jeanjean, Louis
1997
Stabilization with relaxed controls. Zbl 0525.93053
Artstein, Zvi
1983
Critical point theory for asymptotically quadratic functionals and applications to problems with resonance. Zbl 0872.58018
Bartsch, Thomas; Li, Shujie
1997
Existence and multiplicity results for homoclinic solutions to a class of Hamiltonian systems. Zbl 0840.34044
Ding, Yanheng
1995
A nonlinear singular boundary value problem. Zbl 0421.34021
Taliaferro, Steven D.
1979
Global existence of small solutions to a class of nonlinear evolution equations. Zbl 0576.35023
Ponce, Gustavo
1985
A class of De Giorgi type and Hölder continuity. Zbl 0927.46022
Fan, Xianling; Zhao, Dun
1999
Global analysis in some delayed ratio-dependent predator-prey systems. Zbl 0946.34061
Beretta, Edoardo; Kuang, Yang
1998
Solvability of three point boundary value problems at resonance. Zbl 0891.34019
Feng, W.; Webb, J. R. L.
1997
Nonlinear functional differential equations of arbitrary orders. Zbl 0934.34055
El-Sayed, Ahmed M. A.
1998
Existence results for the flow of viscoelastic fluids with a differential constitutive law. Zbl 0729.76006
Guillopé, C.; Saut, J. C.
1990
On global weak solutions for Landau-Lifshitz equations: Existence and nonuniqueness. Zbl 0788.35065
Alouges, François; Soyeur, Alain
1992
The Debye system: Existence and large time behavior of solutions. Zbl 0814.35054
1994
Fixed point theorems for asymptotically nonexpansive mappings. Zbl 0812.47058
Lim, Teck-Cheong; Xu, Hong-Kun
1994
Attractors for the Bénard problem: Existence and physical bounds on their fractal dimension. Zbl 0646.76098
Foias, C.; Manley, O.; Temam, R.
1987
An extension theorem from connected sets, and homogenization in general periodic domains. Zbl 0779.35011
Acerbi, E.; Chiadò Piat, V.; Dal Maso, G.; Percivale, D.
1992
Infinitely many solutions of a symmetric Dirichlet problem. Zbl 0799.35071
Bartsch, Thomas
1993
Clarke’s tangent cones and the boundaries of closed sets in $$\mathbb{R}^n$$. Zbl 0443.26010
Rockafellar, R. T.
1979
On the equation of turbulent filtration in one-dimensional porous media. Zbl 0613.76102
Esteban, Juan R.; Vazquez, Juan L.
1986
Variational elliptic problems which are nonquadratic at infinity. Zbl 0820.35059
Costa, D. G.; Magalhães, C. A.
1994
The global attractor for the 2D Navier-Stokes flow on some unbounded domains. Zbl 0901.35070
Rosa, Ricardo
1998
Variational problems related to self-similar solutions of the heat equation. Zbl 0639.35038
Escobedo, M.; Kavian, O.
1987
Cooperative systems of differential equations with concave nonlinearities. Zbl 0612.34035
Smith, H. L.
1986
Explosive solutions of quasilinear elliptic equations: Existence and uniqueness. Zbl 0793.35028
Díaz, G.; Letelier, R.
1993
One-dimensional transport equations with discontinuous coefficients. Zbl 0989.35130
Bouchut, F.; James, F.
1998
Necessary and sufficient conditions for $$L_ 1$$-strong-weak lower semicontinuity of integral functionals. Zbl 0638.49004
Balder, Erik J.
1987
Fixed point theory in modular function spaces. Zbl 0714.47040
Khamsi, M. A.; Kozlowski, W. M.; Reich, S.
1990
Lipschitzian properties of multifunctions. Zbl 0573.54011
Rockafellar, R. Tyrrell
1985
On optimization problems with prescribed rearrangements. Zbl 0678.49003
Alvino, Angelo; Trombetti, Guido; Lions, Pierre-Louis
1989
Application of hereditary symmetries to nonlinear evolution equations. Zbl 0419.35049
Fuchssteiner, Benno
1979
On cone convexity of set-valued maps. Zbl 0895.26010
Kuroiwa, Daishi; Tanaka, Tamaki; Ha, Truong Xuan Duc
1997
On a problem of Bieberbach and Rademacher. Zbl 0833.35052
Lazer, A. C.; McKenna, P. J.
1993
Singular solutions of some nonlinear elliptic equations. Zbl 0457.35031
Véron, Laurent
1981
Continuity of solutions of a singular parabolic equation. Zbl 0511.35052
Sacks, Paul E.
1983
Stability for multispecies population models in random environments. Zbl 0598.92017
Gard, Thomas C.
1986
Semilinear integrodifferential equations with nonlocal Cauchy problem. Zbl 0916.45014
Lin, Yanping; Liu, James H.
1996
Decay, symmetry and existence of solutions of semilinear elliptic systems. Zbl 0938.35054
de Figueiredo, Djairo G.; Yang, Jianfu
1998
Vector variational inequality as a tool for studying vector optimization problems. Zbl 0956.49007
Lee, Gue Myung; Kim, Do Sang; Lee, Byung Soo; Yen, Nguyen Dong
1998
Some problems and results in the study of nonlinear analysis. Zbl 0901.47036
Chang, Shihsen
1997
Existence and uniqueness of “entropy” solutions of parabolic problems with $$L^1$$ data. Zbl 0909.35075
Prignet, Alain
1997
Global smooth thermomechanical processes in one-dimensional nonlinear thermoviscoelasticity. Zbl 0498.35015
Dafermos, C. M.; Hsiao, L.
1982
Existence and convergence for fixed points of mappings of asymptotically nonexpansive type. Zbl 0747.47041
Xu, Hong-Kun
1991
An iterative procedure for constructing zeros of accretive sets in Banach spaces. Zbl 0375.47032
Reich, Simeon
1978
Finite element methods for parabolic and hyperbolic partial integro- differential equations. Zbl 0657.65142
Yanik, Elizabeth G.; Fairweather, Graeme
1988
Existence of solutions to a semilinear functional-differential evolution nonlocal problem. Zbl 0934.34068
Byszewski, Ludwik; Akca, Haydar
1998
A general approach to critical Fujita exponents in nonlinear parabolic problems. Zbl 1139.35317
Galaktionov, Victor A.; Levine, Howard A.
1998
A mountain pass method for the numerical solution of semilinear elliptic problems. Zbl 0779.35032
Choi, Y. S.; McKenna, P. J.
1993
Metric regularity, openness and Lipschitzian behavior of multifunctions. Zbl 0687.54015
Penot, Jean-Paul
1989
Multiplicity results for a fourth-order semilinear elliptic problem. Zbl 0898.35032
Micheletti, Anna Maria; Pistoia, Angela
1998
Equations with unbounded delay: A survey. Zbl 0449.34048
Corduneanu, C.; Lakshmikantham, V.
1980
Convergence theorems of the sequence of iterates for asymptotically demicontractive and hemicontractive mappings. Zbl 0861.47047
Liu, Qihou
1996
Nontrivial solutions of operator equations and Morse indices of critical points of min-max type. Zbl 0667.47036
Lazer, A. C.; Solimini, S.
1988
A parabolic equation with nonlocal boundary conditions arising from electrochemistry. Zbl 0757.35031
Choi, Y. S.; Chan, Kwong-Yu
1992
Stochastic Cahn-Hilliard equation. Zbl 0838.60056
Da Prato, Giuseppe; Debussche, Arnaud
1996
Coercive and semicoercive hemivariational inequalities. Zbl 0733.49012
Panagiotopoulos, P. D.
1991
Dynamic theory of quasilinear parabolic equations: Abstract evolution equations. Zbl 0666.35043
Amann, Herbert
1988
Fisher wave fronts for the Lotka-Volterra competition model with diffusion. Zbl 0868.35053
Kan-On, Yukio
1997
A class of similarity solutions of the nonlinear diffusion equation. Zbl 0394.34016
van Duyn, C. J.; Peletier, L. A.
1977
On the bounded solutions of a nonlinear convolution equation. Zbl 0433.92028
Diekmann, Odo; Kaper, Hans G.
1978
S-shaped bifurcation curves. Zbl 0458.35036
Brown, K. J.; Ibrahim, M. M. A.; Shivaji, R.
1981
Global stability and predator dynamics in a model of prey dispersal in a patchy environment. Zbl 0685.92018
Freedman, H. I.; Takeuchi, Y.
1989
On Hopf’s formulas for solutions of Hamilton-Jacobi equations. Zbl 0569.35011
Bardi, M.; Evans, L. C.
1984
On symmetric solutions of an elliptic equation with a nonlinearity involving critical Sobolev exponent. Zbl 0823.35051
Bianchi, Gabriele; Chabrowski, Jan; Szulkin, Andrzej
1995
Strong convergence theorems for asymptotically nonexpansive semigroups in Hilbert spaces. Zbl 0935.47039
Shioji, Naoki; Takahashi, Wataru
1998
Positive solutions for $$(n-1,1)$$ conjugate boundary value problems. Zbl 0871.34015
Eloe, Paul W.; Henderson, Johnny
1997
Linking theorems and applications to semilinear elliptic problems at resonance. Zbl 0731.35042
Silva, Elves Alves de B. e
1991
Existence and uniqueness results for dynamic contact problems with nonlinear normal and friction interface laws. Zbl 0672.73079
Martins, J. A. C.; Oden, J. T.
1987
On an $$m$$-point boundary value problem. Zbl 0895.34014
Feng, Wenying
1997
Some existence and multiplicity results for a class of quasilinear elliptic eigenvalue problems. Zbl 0782.35053
Guo, Zongming
1992
Extrema problems with critical Sobolev exponents on unbounded domains. Zbl 0851.49004
Ben-Naoum, A. K.; Troestler, C.; Willem, M.
1996
Well-posedness criteria in optimization with application to the calculus of variations. Zbl 0841.49005
Zolezzi, T.
1995
A proof of Trudinger’s inequality and its application to nonlinear Schrödinger equations. Zbl 0715.35073
Ogawa, Takayoshi
1990
Razumikhin type stability theorems for impulsive functional differential equations. Zbl 0933.34083
Shen, Jianhua; Yan, Jurang
1998
Approximative methods for nonlinear equations (two approaches to the convergence problem). Zbl 0401.65034
Vainikko, G.
1978
Global existence of periodic solutions in a class of delayed Gause-type predator-prey systems. Zbl 0872.34047
Zhao, Tao; Kuang, Yang; Smith, H. L.
1997
Some remarks on the wave equations with nonlinear damping and source terms. Zbl 0866.35071
Ikehata, Ryo
1996
An existence theorem for a nonlinear difference equation. Zbl 0774.39001
Cheng, Sui Sun; Patula, William T.
1993
Evolution equations with lack of convexity. Zbl 0545.46029
Degiovanni, Marco; Marino, Antonio
1985
Existence results for perturbations of the $$p$$-Laplacian. Zbl 0818.35029
Costa, David G.; Magalhães, Celius A.
1995
Strongly nonlinear elliptic equations having natural growth terms and $$L^ 1$$ data. Zbl 0795.35031
Boccardo, L.; Gallouet, T.
1992
A predator-prey model with disease in the prey. Zbl 0922.34036
1999
A class of De Giorgi type and Hölder continuity. Zbl 0927.46022
Fan, Xianling; Zhao, Dun
1999
The initial value problem for a generalized Boussinesq model. Zbl 0930.35136
Lorca, Sebastián A.; Boldrini, José Luiz
1999
The study of maximal elements, fixed points for $$L_S$$-majorized mappings and their applications to minimax and variational inequalities in product topological spaces. Zbl 0930.47024
Deguire, Paul; Tan, Kok Keong; Yuan, George Xian-Zhi
1999
Impulsive controllability and optimization problems in population dynamics. Zbl 0941.49021
Nenov, Svetoslav
1999
A density result in SBV with respect to non-isotropic energies. Zbl 0939.49024
1999
Impulsive stabilization of functional differential equations by Lyapunov-Razumikhin functions. Zbl 0951.34049
Yan, Jurang; Shen, Jianhua
1999
A high-linking algorithm for sign-changing solutions of semilinear elliptic equations. Zbl 0941.35023
Ding, Zhonghai; Costa, David; Chen, Goong
1999
Existence results for the problem $$(\varphi(u'))'= f(t,u,u')$$ with nonlinear boundary conditions. Zbl 0920.34029
1999
An existence theorem for a strongly nonlinear elliptic problem in Orlicz spaces. Zbl 0920.35057
Benkirane, A.; Elmahi, A.
1999
Razumikhin techniques in impulsive functional differential equations. Zbl 0939.34071
Shen, J. H.
1999
On essential components of the set of Nash equilibrium points. Zbl 0967.91004
Yu, Jian; Xiang, Shuwen
1999
A survey of subdifferential calculus with applications. Zbl 0933.49006
Borwein, Jonathan M.; Zhu, Qiji J.
1999
Global stability of discrete models of Lotka-Volterra type. Zbl 0919.92030
Wang, Wendi; Lu, Zhengyi
1999
Conservation laws with vanishing nonlinear diffusion and dispersion. Zbl 0923.35159
LeFloch, Philippe G.; Natalini, Roberto
1999
Infinitely many homoclinic orbits of a Hamiltonian system with symmetry. Zbl 0938.37034
Ding, Yanheng; Girardi, Mario
1999
A Lyapunov characterization of robust stabilization. Zbl 0947.34054
Ledyaev, Yuri S.; Sontag, Eduardo D.
1999
Theory and applications of Hopf bifurcations in symmetric functional differential equations. Zbl 0917.58027
Krawcewicz, Wiesław; Wu, Jianhong
1999
A note on existence of nonnegative solutions to singular semi-positone problems. Zbl 0921.34027
Agarwal, Ravi P.; O’Regan, Donal
1999
Strong maximum principles for supersolutions of quasilinear elliptic equations. Zbl 0930.35074
Montenegro, Marcelo
1999
Large solutions of semilinear elliptic problems. Zbl 0932.35081
Lair, Alan V.; Wood, Aihua W.
1999
Extremal solutions of a discontinuous scalar differential equation. Zbl 0949.34005
1999
Uniqueness criterion of weak solutions to the stationary Navier-Stokes equations in exterior domains. Zbl 0934.35123
Kozono, Hideo; Yamazaki, Masao
1999
Hamiltonian symmetric groups and multiple periodic solutions to delay differential equations. Zbl 0920.34061
Li, Jibin; He, Xue-Zhong; Liu, Zhengrong
1999
Existence and uniform decay of solutions of a degenerate equation with nonlinear boundary damping and boundary memory source term. Zbl 0933.35157
Cavalcanti, M. M.; Domingos Cavalcanti, V. N.; Prates Filho, J. S.; Soriano, J. A.
1999
Persistence and global stability for two-species nonautonomous competition Lotka-Volterra patch-system with time delay. Zbl 0949.34060
Zhang, Jingru; Chen, Lansun; Chen, Xiu Dong
1999
Fixed point theory in symmetric spaces with applications to probabilistic spaces. Zbl 0947.54022
Hicks, Troy L.; Rhoades, B. E.
1999
On parabolic hemivariational inequalities and applications. Zbl 0923.35089
Miettinen, M.; Panagiotopoulos, P. D.
1999
Global asymptotic stability of a predator-prey system of Holling type. Zbl 0984.34043
Sugie, Jitsuro; Katayama, Masaki
1999
Existence theory for nonlinear Fredholm and Volterra integral equations on half-open intervals. Zbl 0920.45006
Meehan, Maria; O’Regan, Donal
1999
A weighted equation approach to decay rate estimates for the Navier-Stokes equations. Zbl 0941.35066
Takahashi, Shuji
1999
A criterion for existence of positive solutions of systems of retarded functional differential equations. Zbl 0935.34061
Diblík, Josef
1999
Existence of quasiperiodic solutions and Littlewood’s boundedness problem of Duffing equations with subquadratic potentials. Zbl 0927.34021
Küpper, Tassilo; You, Jiangong
1999
Fixed point theorems in hyperconvex metric spaces. Zbl 0930.47023
Park, Sehie
1999
The discrete Markus-Yamabe problem. Zbl 0919.34042
Cima, Anna; Gasull, Armengol; Mañosas, Francesc
1999
Second order impulsive integro-differential equations on unbounded domains in Banach spaces. Zbl 0917.45010
Guo, Dajun
1999
Asymptotic behavior for an SIS epidemic model and its approximation. Zbl 0921.92029
Iannelli, Mimmo; Kim, Mi-Young; Park, Eun-Jae
1999
Coderivatives of multivalued mappings, locally compact cones and metric regularity. Zbl 0919.46031
Jourani, A.; Thibault, L.
1999
A class of evolution hemivariational inequalities. Zbl 0920.47056
Liu, Zhenhai
1999
The metallic means family and multifractal spectra. Zbl 0931.28007
1999
On weak solutions for an evolution equation with exponential nonlinearities. Zbl 0940.35033
Ma, T. F.; Soriano, J. A.
1999
Self-similar large time behavior of solutions to Korteweg-de Vries-Burgers equation. Zbl 0923.35158
Karch, Grzegorz
1999
A nonlinear suspension bridge equation with nonconstant load. Zbl 0934.74031
Choi, Q. Heung; Jung, Tacksun
1999
Existence and nonexistence of global solutions for the generalized IMBq equation. Zbl 0920.35005
Chen, Guowang; Wang, Shubin
1999
$$G$$-convergence of parabolic operators. Zbl 0933.35020
Svanstedt, Nils
1999
Topological degree and periodic solutions of differential inclusions. Zbl 0936.34009
De Blasi, Francesco S.; Górniewicz, Lech; Pianigiani, Giulio
1999
Existence and nonexistence of positive radial solutions for a class of semilinear elliptic systems. Zbl 0934.34011
Chen, Shaohua; Lu, Guozhen
1999
Positive radial solutions of quasilinear elliptic partial differential equations on a ball. Zbl 0924.35047
García-Huidobro, M.; Manásevich, R.; Schmitt, K.
1999
Convergence of generic infinite products of nonexpansive and uniformly continuous operators. Zbl 0932.47043
Reich, Simeon; Zaslavski, Alexander J.
1999
Positive solutions to semilinear problems with coefficients that changes sign. Zbl 0930.35069
Các, Nguyen Phuong; Gatica, Juan A.; Li, Yi
1999
Existence results for nonlinear problems with separated boundary conditions. Zbl 0918.34021
1999
On a Hartman linearization theorem for a class of ODE with impulse effect. Zbl 0931.34007
Fenner, Julio López; Pinto, Manuel
1999
Bifurcations of periodic orbits, subharmonic solutions and invariant tori of high-dimensional systems. Zbl 0922.34035
Han, Maoan; Jiang, Katie; Green, David jun.
1999
Strong convergence theorems for nonexpansive type and non-self multi-valued mappings. Zbl 0938.47039
Sahu, D. R.
1999
Periodic solutions for evolution equations. Zbl 0924.34034
Li, Yong; Cong, Fuzhong; Lin, Zhenghua; Liu, Wenbin
1999
Approximate generalized Hessians and Taylor’s expansions for continuously Gâteaux differentiable functions. Zbl 0931.49011
Jeyakumar, V.; Yang, X. Q.
1999
Nontrivial solutions for resonant cooperative elliptic systems via computations of critical groups. Zbl 0940.35074
Zou, Wenming; Li, Shujie; Liu, J. Q.
1999
Bifurcation of a periodic orbit from infinity in planar piecewise linear vector fields. Zbl 1049.34052
Llibre, Jaume; Ponce, Enrique
1999
Iterative solutions of nonlinear accretive operator equations in arbitrary Banach spaces. Zbl 0935.47035
Chidume, C. E.; Osilike, M. O.
1999
Existence of solutions of the equation $$u_t=\Delta\log u$$. Zbl 0936.35098
Hui, Kin Ming
1999
Feedback stabilization for a class of distributed semilinear control systems. Zbl 0946.93036
Bounit, H.; Hammouri, H.
1999
Stability and instability of solitary waves for a nonlinear dispersive system. Zbl 0923.35153
Alarcon, Eduardo; Angulo, Jaime; Montenegro, Jose F.
1999
A nonlinear boundary value problem arising in growing cell populations. Zbl 0935.35170
Latrach, Khalid; Jeribi, Aref
1999
Approximate controllability of a semilinear heat equation in unbounded domains. Zbl 0946.93006
de Teresa, Luz; Zuazua, Enrique
1999
Positive solutions for semilinear elliptic equations in annular domains. Zbl 1034.35044
Hai, D. D.
1999
The blow-up rate for a system of heat equations completely coupled in the boundary conditions. Zbl 0919.35062
Wang, Shu; Xie, Chunhong; Wang, Mingxin
1999
Iterative solutions of nonlinear $$\phi$$-strongly accretive operator equations in arbitrary Banach spaces. Zbl 0927.47036
Osilike, M. O.
1999
The study of equilibria for abstract economics in topological vector spaces – a unified approach. Zbl 0943.47053
Yuan, George Xian-Zhi
1999
Stable curves asymptotic to a degenerate fixed point. Zbl 0918.58064
Fontich, E.
1999
On relations and applications of generalized second-order directional derivatives. Zbl 0990.49016
Yang, X. Q.
1999
Nonnegative solutions to some singular second-order boundary value problems. Zbl 0929.34022
Kelevedjiev, Petio
1999
Multiple positive solutions for a class of semilinear elliptic boundary value problems. Zbl 0933.35075
Maya, C.; Shivaji, R.
1999
Excitability of a second-order delay differential equation. Zbl 0945.34048
Wiener, Joseph; Lakshmikantham, V.
1999
Initial value problems for second-order integro-differential equations in Banach spaces. Zbl 0931.34042
Guo, Dajun
1999
On a nonlinear fluid-structure interaction problem defined on a domain depending on time. Zbl 0938.35116
Flori, Fabien; Orenga, Pierre
1999
Scalar nonlinear conservation laws with integrable boundary data. Zbl 0919.35081
Ancona, Fabio; Marson, Andrea
1999
$$L^p$$ solutions to the time-dependent Ginzburg-Landau equations of superconductivity. Zbl 0919.35128
Wang, Shouhong; Zhan, Mei-Qin
1999
Generalized quasilinearization method for second-order boundary value problems. Zbl 0922.34018
Mohapatra, R. N.; Vajravelu, K.; Yin, Y.
1999
The zero relaxation limit for $$2\times 2$$ hyperbolic systems. Zbl 0935.35099
1999
On the damped Boussinesq equation in a circle. Zbl 0938.35146
1999
Geodesics in static spacetimes and $$t$$-periodic trajectories. Zbl 0982.53038
Sánchez, Miguel
1999
Uniform persistence and global asymptotic stability in periodic single-species models of dispersal in a patchy environment. Zbl 0927.34027
Freedman, H. I.; Peng, Qui-Liang
1999
Maximal elements and equilibria for condensing correspondences. Zbl 0946.47038
Chebbi, Souhail; Florenzano, Monique
1999
Growth and decay results in heat conduction problems with nonlinear boundary conditions. Zbl 0919.35066
Payne, L. E.; Schaefer, P. W.; Song, J. C.
1999
Maluta’s coefficient and Opial’s properties in Musielak-Orlicz sequence spaces equipped with the Luxemburg norm. Zbl 0922.46005
Cui, Yunan; Hudzik, Henryk
1999
On a new type of bifurcation of limit cycles for a planar cubic system. Zbl 0917.34021
Chavarriga, Javier; Giacomini, H.; Giné, Jaume
1999
A quasistatic contact problem for an elastic perfectly plastic body with Tresca’s friction. Zbl 0923.73054
Amassad, Amina; Shillor, Meir; Sofonea, Mircea
1999
Bifurcation for an elliptic system coupled in the linear part. Zbl 0939.35066
Fleckinger, Jacqueline; Pardo San Gil, Rosa
1999
Optimal investment with taxes: An optimal control problem with endogeneous delay. Zbl 1126.91370
Jouini, Elyès; Koehl, Pierre-F.; Touzi, Nizar
1999
Approximation of the zeros of $$m$$-accretive operators. Zbl 0942.47038
Chidume, C. E.; Zegeye, Habtu
1999
The solution by iteration of nonlinear equations involving psi-strongly accretive operators. Zbl 0931.47037
Moore, Chika
1999
On a degenerate parabolic/hyperbolic system in glaciology giving rise to a free boundary. Zbl 0935.35179
Diaz, J. I.; Schiavi, E.
1999
Boundedness and blow-up behavior for reaction-diffusion systems in a bounded domain. Zbl 0932.35125
Zhang, Jian
1999
Existence and uniqueness results for polyharmonic equations. Zbl 0921.35058
Dalmasso, Robert
1999
Positive solutions for a semilinear elliptic problem with sign-changing nonlinearity. Zbl 0930.35068
Afrouzi, G. A.; Brown, K. J.
1999
Yamabe equations on half-spaces. Zbl 0941.35025
Bianchi, Gabriele; Pan, Xing-Bin
1999
Iterative schemes for optimal control of Volterra integral equations. Zbl 0936.49016
Belbas, S. A.
1999
Generalized solutions to nonlinear Volterra integral equations with non-Lipschitz nonlinearity. Zbl 0931.45005
Pilipović, S.; Stojanović, M.
1999
Multiple positive solutions of quasilinear elliptic equations in $$\mathbb{R}^N$$. Zbl 0930.35062
Drábek, Pavel; Huang, Yin Xi
1999
Some degree calculations and applications to global bifurcation of variational inequalities. Zbl 0928.49009
Le, Vy Khoi
1999
...and 1467 more Documents
all top 5

### Cited by 21,674 Authors

 292 Papageorgiou, Nikolaos S. 276 Agarwal, Ravi P. 232 O’Regan, Donal 131 Ge, Weigao 116 Yao, Jen-Chih 115 Tang, Xianhua 103 Rădulescu, Vicenţiu D. 98 Alves, Claudianor Oliveira 95 Kumam, Poom 80 Benchohra, Mouffak 80 Chang, Shih-Sen 79 Guo, Boling 78 Henderson, Johnny Lee 78 Li, Wan-Tong 76 Gasiński, Leszek 74 Cho, Yeol Je 74 Nieto Roig, Juan Jose 74 Reich, Simeon 72 Ma, Ruyun 71 Jiang, Daqing 69 Li, Yongxiang 69 Wang, Mingxin 66 Wong, Patricia J. Y. 65 Chidume, Charles Ejike 64 Boccardo, Lucio 64 Miyagaki, Olimpio Hiroshi 63 Chen, Lansun 62 Kang, Shin Min 61 Ceng, Lu-Chuan 61 Ezzinbi, Khalil 61 Liu, Lishan 60 Motreanu, Dumitru 60 Yuan, Rong 59 Mu, Chunlai 59 Shahzad, Naseer 57 Pao, Chia-Ven 57 Yang, Zuodong 56 Huang, Nan-Jing 56 Lakshmikantham, Vangipuram 56 Vazquez, Juan Luis 55 Tang, Chun-Lei 53 Khamsi, Mohamed Amine 53 Penot, Jean-Paul 52 Zanolin, Fabio 51 López-Gómez, Julián 51 Thibault, Lionel 51 Wu, Yonghong 49 Balachandran, Krishnan 49 Schechter, Martin 49 Takahashi, Wataru 49 Zou, Wenming 48 Cabada, Alberto 48 Lu, Shiping 48 Nguyen Thanh Long 48 Shivaji, Ratnasingham 48 Xu, Hong-Kun 47 Ansari, Qamrul Hasan 47 Liu, Zhenhai 47 Zaslavski, Alexander Yakovlevich 46 Graef, John R. 46 Zegeye, Habtu 45 Carl, Siegfried 45 Ding, Xie Ping 45 Drábek, Pavel 45 Mordukhovich, Boris S. 45 Teng, Zhi-dong 44 Zhang, Weinian 43 Figueiredo, Giovany Malcher 43 Yang, Minbo 42 Llibre, Jaume 42 Zhang, Jihui 41 Diaz Diaz, Jesus Ildefonso 41 Valls Anglés, Cláudia 41 Véron, Laurent 41 Xu, Rui 40 Chen, Haibo 40 Abreu Goncalves, Jose Valdo 40 Huang, Lihong 40 Lin, Lai-Jiu 40 Shehu, Yekini 40 Winkler, Michael 40 Yu, Jian-She 39 Ozawa, Tohru 39 Wu, Xian 38 Choi, Q-Heung 38 Park, Jong Yeoul 38 Zheng, Sining 37 Qin, Xiaolong 37 Sofonea, Mircea 37 Sugie, Jitsuro 37 Titi, Edriss Saleh 37 Wang, Yuanming 36 Liu, Xinzhi 36 Peletier, Lambertus Adrianus 36 Peral Alonso, Ireneo 36 Wang, Jinrong 36 Wang, Ke 36 Yin, Jingxue 35 Omari, Pierpaolo 35 Wu, Jianhong ...and 21,574 more Authors
all top 5

### Cited in 869 Journals

 2,803 Journal of Mathematical Analysis and Applications 2,637 Nonlinear Analysis. Theory, Methods & Applications. Series A: Theory and Methods 1,583 Journal of Differential Equations 1,488 Nonlinear Analysis. Theory, Methods & Applications 862 Applied Mathematics and Computation 648 Computers & Mathematics with Applications 533 Applicable Analysis 474 Nonlinear Analysis. Real World Applications 435 Applied Mathematics Letters 428 Boundary Value Problems 408 Abstract and Applied Analysis 389 Journal of Optimization Theory and Applications 380 Fixed Point Theory and Applications 361 Journal of Computational and Applied Mathematics 326 Calculus of Variations and Partial Differential Equations 303 Proceedings of the American Mathematical Society 281 Advances in Difference Equations 277 Mathematical Methods in the Applied Sciences 269 Archive for Rational Mechanics and Analysis 269 Annali di Matematica Pura ed Applicata. Serie Quarta 268 Transactions of the American Mathematical Society 265 Communications in Partial Differential Equations 260 Mathematical and Computer Modelling 253 Numerical Functional Analysis and Optimization 249 Journal of Functional Analysis 246 Annales de l’Institut Henri Poincaré. Analyse Non Linéaire 230 Journal of Mathematical Physics 229 Journal of Inequalities and Applications 222 Optimization 221 Discrete and Continuous Dynamical Systems 218 Proceedings of the Royal Society of Edinburgh. Section A. Mathematics 200 ZAMP. Zeitschrift für angewandte Mathematik und Physik 187 NoDEA. Nonlinear Differential Equations and Applications 180 Communications on Pure and Applied Analysis 178 Chaos, Solitons and Fractals 166 Acta Mathematica Sinica. English Series 163 Journal of Fixed Point Theory and Applications 162 International Journal of Bifurcation and Chaos in Applied Sciences and Engineering 157 Journal de Mathématiques Pures et Appliquées. Neuvième Série 151 Discrete and Continuous Dynamical Systems. Series B 150 Rocky Mountain Journal of Mathematics 147 Bulletin of the Australian Mathematical Society 147 Journal of Applied Mathematics and Computing 145 Physica D 143 Journal of Difference Equations and Applications 138 Applied Mathematics and Mechanics. (English Edition) 138 Acta Applicandae Mathematicae 137 Journal of Global Optimization 136 Journal of Dynamics and Differential Equations 135 Acta Mathematicae Applicatae Sinica. English Series 135 M$$^3$$AS. Mathematical Models & Methods in Applied Sciences 133 Communications in Contemporary Mathematics 129 Journal of Mathematical Sciences (New York) 128 Complex Variables and Elliptic Equations 126 Mediterranean Journal of Mathematics 120 Applied Mathematics and Optimization 120 Advanced Nonlinear Studies 110 SIAM Journal on Mathematical Analysis 108 Systems & Control Letters 108 European Series in Applied and Industrial Mathematics (ESAIM): Control, Optimization and Calculus of Variations 106 Zeitschrift für Analysis und ihre Anwendungen 106 Journal of Applied Mathematics 105 Communications in Nonlinear Science and Numerical Simulation 98 Applied Numerical Mathematics 94 Discrete Dynamics in Nature and Society 94 Discrete and Continuous Dynamical Systems. Series S 94 Set-Valued and Variational Analysis 92 Journal of Function Spaces 91 Automatica 89 Journal of Evolution Equations 88 Journal of Mathematical Biology 88 Mathematische Nachrichten 88 Advances in Nonlinear Analysis 87 Mathematical Biosciences 85 Communications in Mathematical Physics 82 Czechoslovak Mathematical Journal 81 Mathematische Annalen 81 Mathematical Programming. Series A. Series B 81 Nonlinear Dynamics 79 Topological Methods in Nonlinear Analysis 78 Manuscripta Mathematica 78 Applications of Mathematics 78 Applied Mathematics. Series B (English Edition) 76 Comptes Rendus. Mathématique. Académie des Sciences, Paris 75 Advances in Mathematics 73 Annali della Scuola Normale Superiore di Pisa. Classe di Scienze. Serie IV 73 Set-Valued Analysis 72 Applied Mathematical Modelling 71 Mathematical Notes 70 Israel Journal of Mathematics 70 Mathematische Zeitschrift 70 Positivity 69 Results in Mathematics 66 Stochastic Analysis and Applications 66 Differential Equations 63 Monatshefte für Mathematik 63 Filomat 62 Nonlinearity 61 Differential Equations and Dynamical Systems 61 Journal of Mathematical Fluid Mechanics ...and 769 more Journals
all top 5

### Cited in 63 Fields

 15,351 Partial differential equations (35-XX) 7,751 Ordinary differential equations (34-XX) 5,577 Operator theory (47-XX) 3,639 Calculus of variations and optimal control; optimization (49-XX) 2,688 Biology and other natural sciences (92-XX) 2,486 Numerical analysis (65-XX) 2,308 Dynamical systems and ergodic theory (37-XX) 2,015 Fluid mechanics (76-XX) 1,623 Global analysis, analysis on manifolds (58-XX) 1,412 Operations research, mathematical programming (90-XX) 1,380 Systems theory; control (93-XX) 1,183 Functional analysis (46-XX) 1,119 Mechanics of deformable solids (74-XX) 1,068 Integral equations (45-XX) 968 General topology (54-XX) 915 Difference and functional equations (39-XX) 805 Real functions (26-XX) 763 Probability theory and stochastic processes (60-XX) 472 Mechanics of particles and systems (70-XX) 451 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 443 Statistical mechanics, structure of matter (82-XX) 383 Differential geometry (53-XX) 346 Classical thermodynamics, heat transfer (80-XX) 252 Optics, electromagnetic theory (78-XX) 229 Quantum theory (81-XX) 175 Measure and integration (28-XX) 158 Potential theory (31-XX) 150 Harmonic analysis on Euclidean spaces (42-XX) 135 Approximations and expansions (41-XX) 129 Convex and discrete geometry (52-XX) 126 Statistics (62-XX) 114 Computer science (68-XX) 102 Geophysics (86-XX) 100 Algebraic topology (55-XX) 84 Functions of a complex variable (30-XX) 75 Relativity and gravitational theory (83-XX) 68 Linear and multilinear algebra; matrix theory (15-XX) 58 Information and communication theory, circuits (94-XX) 54 Several complex variables and analytic spaces (32-XX) 48 Abstract harmonic analysis (43-XX) 46 Manifolds and cell complexes (57-XX) 42 History and biography (01-XX) 42 Mathematical logic and foundations (03-XX) 42 Combinatorics (05-XX) 37 Algebraic geometry (14-XX) 34 Integral transforms, operational calculus (44-XX) 31 Order, lattices, ordered algebraic structures (06-XX) 30 Special functions (33-XX) 28 General and overarching topics; collections (00-XX) 28 Astronomy and astrophysics (85-XX) 21 Topological groups, Lie groups (22-XX) 16 Nonassociative rings and algebras (17-XX) 16 Sequences, series, summability (40-XX) 13 Group theory and generalizations (20-XX) 12 Geometry (51-XX) 11 Commutative algebra (13-XX) 9 Number theory (11-XX) 7 Field theory and polynomials (12-XX) 3 $$K$$-theory (19-XX) 2 Associative rings and algebras (16-XX) 2 Mathematics education (97-XX) 1 General algebraic systems (08-XX) 1 Category theory; homological algebra (18-XX)