O Modelo de Gestão: um estudo de caso em uma Organização Militar Prestadora de Serviço na área industrial da Marinha do Brasil

O estudo da gestão no âmbito organizacional mostra-se significativo para o entendimento das relações que se dão nas empresas e para o desenvolvimento organizacional, o que torna imprescindível sua análise no campo de estudos das práticas gerenciais, no intuito de melhor entender como práticas de gestão mais apuradas poderão melhorar o desempenho das organizações e fazê-las, assim, atingir suas metas e resultados almejados. Uma das maneiras pelas quais o Estado procura alcançar seus resultados é por meio da implementação de Políticas Públicas. No estudo da administração, é crucial que se busque o equilíbrio das dimensões políticas, organizacionais e legais desses processos. Esta pesquisa objetiva verificar o atual sistema de gestão utilizado pelo Arsenal de Marinha do Rio de Janeiro (AMRJ), uma Organização Militar Prestadora de Serviço (OMPS), que, embora seja considerada uma OMPS industrial (OMPS-I), possui uma tríplice atribuição: manutenção de meios navais, apoio de base e construção naval. Logo, são verificados os atuais óbices na sua gestão, assim como suas potencialidades, no nível estratégico, e a aplicabilidade de ferramenta gerencial que possa subsidiar a gestão estratégica da OM. O questionamento se direciona para quais aspectos, na forma de ameaças e fraquezas, influenciam na gestão do AMRJ e quais alternativas poderiam ser propostas para otimizar a sua gestão e minimizar as disfunções encontradas? Sendo assim, para que o AMRJ possa cumprir sua missão com eficiência, efetividade, economicidade e eficácia, torna-se crucial um exame do sistema atual de sua gestão, concernente à condução de suas atividades. Trata-se de uma pesquisa exploratória e descritiva, qualitativa, dedutiva, tendo sido utilizado o método de estudo de caso com pesquisa de campo e bibliográfica. Pode-se perceber que muitas são as limitações e ameaças, entretanto são significativos os pontos fortes e as oportunidades. O que norteou a pesquisa foi a busca pela maximização do resultado global da OM. Procurando ajustar o conjunto de elementos organizacionais que compõem a estrutura do AMRJ, de modo a atingir sinergia da ação isolada, porém sob a mesma orientação estratégica, de modo a permitir um alcance da efetividade, da eficácia e maior eficiência para essa importante OM pertencente à Marinha do Brasil.

Cooperação técnica entre os órgãos de controle externo e de controle interno: uma percepção dos servidores do município do Rio de Janeiro

O desenvolvimento da sociedade e da economia requer adaptações necessárias na gestão pública, visando atender aos anseios da coletividade: melhores serviços públicos e a efetiva entrega, com qualidade, dos produtos de suas ações ao cliente-cidadão, alcançando assim o princípio da eficiência. Na extensão em que a quantidade e a complexidade das operações efetuadas pela gestão pública crescem, ampliam-se também os seus riscos. Desta forma, as ações do sistema de controle devem ser intensificadas, sendo possível obter excelentes resultados, com a cooperação técnica entre os órgãos de controle externo e interno. Neste sentido, este estudo teve por objetivo avaliar a percepção dos servidores do município do Rio de Janeiro com atuação no Tribunal de Contas do Município do Rio de Janeiro TCMRJ e na Controladoria Geral do Município CGM, se a sinergia entre os órgãos de controle externo e controle interno, contribui para o aprimoramento do controle na gestão pública municipal. Com o propósito de atender a este objetivo, foi realizada uma pesquisa de natureza descritiva, quantitativa, dedutiva e aplicada. Os dados foram obtidos através de um questionário de pesquisa, disponibilizados na rede intranet da Secretaria Geral de Controle Externo TCMRJ e da CGM. A amostra vinculou-se ao universo dos servidores públicos, com nível de escolaridade ensino médio e superior, gerando 138 respondentes da pesquisa. No que concerne ao resultado, quanto à questão norteadora da pesquisa, 95% dos respondentes da pesquisa concordam que é importante a cooperação técnica entre o TCMRJ e a CGM, para a contribuição do aprimoramento do controle na gestão pública municipal.

Estudo comparativo entre a metodologia do ensino à distância, no âmbito do Consórcio Cederj e a presencial com enfoque nas disciplinas de contabilidade dos cursos de Administração da UFRRJ

Com o advento da internet o ensino a distância se apresenta como uma perspectiva de formação para milhares de cidadãos, permitindo a interiorização do ensino de qualidade e levando a oportunidade de formação àqueles que estão localizados longe dos grandes centros. O ensino a distância permite derrubar as barreiras geográficas que mantém o aluno do interior do Estado apartado do acesso ao ensino público gratuito e de qualidade. No entanto, a aplicação da metodologia EaD deve ser feita de forma a respeitar as características locais sem prescindir dos princípios que o norteiam. A carência de profissionais de contabilidade na esfera pública é significativa. Desta forma, esse trabalho se insere na perspectiva de avaliar se a metodologia da EaD apresenta alguma diferença para o ensino de contabilidade. Através de pesquisa caracterizada em sua metodologia como descritiva, realizada de forma quantitativa que emprega lógica dedutiva, resultante em uma pesquisa aplicada, é traçado um paralelo entre o ensino a distância e o ensino presencial por meio do estudo das disciplinas de contabilidade ministradas nos cursos de Administração da UFRRJ, observando que o curso a distância é oferecido no âmbito do Consórcio Cederj. Através de um conjunto de questionários, foi traçado o perfil do aluno cursista e dos potenciais alunos que ingressarão no curso, bem como a percepção que eles têm da carreira de contador. Foi desenvolvido um estudo sistemático da eficiência das ferramentas oferecidas pela metodologia do EaD como facilitador da aprendizagem, bem como a comparação entre a metodologia do ensino a distância e o presencial, tanto sob a ótica dos alunos quanto do professores. Entre as conclusões verifica-se, através das cidades investigadas, que a população do interior do Estado, prestes a ingressar em um curso superior, desconhece ou tem uma noção muito superficial da profissão de contador e não tem interesse pela carreira de ciências contábeis como opção para o vestibular. Outra conclusão que a pesquisa revela demonstra que a metodologia do EaD é uma poderosa ferramenta para capilarizar o ensino, seja a formação superior como também a formação continuada, sem perda de qualidade para metodologia presencial.

Alfabetização matemática nos anos iniciais do ensino fundamental: uma leitura dos resultados da Pesquisa GERES 2005

O presente estudo teve como objetivo geral compreender o processo de aprendizagem da matemática de estudantes durante o ciclo de alfabetização na cidade do Rio de Janeiro. Para isso, fez-se uso dos dados de uma pesquisa longitudinal, denominada Estudo Longitudinal da Geração Escolar 2005 GERES 2005. Esta Pesquisa consistiu em um estudo de painel que acompanhou ao longo de quatro anos consecutivos (de 2005 a 2008) uma amostra de estudantes do primeiro segmento do Ensino Fundamental (1 à 4 série e/ou 2 ao 5 ano) em cinco cidades brasileiras - Rio de Janeiro, Belo Horizonte, Campinas, Campo Grande e Salvador, por meio de testes de Matemática e Leitura aplicados aos estudantes e de questionários contextuais aplicados a seus professores, aos diretores das escolas, e aos pais. Especificamente o estudo concentrou-se sobre os dados referentes à rede municipal do Rio de Janeiro e mais especificamente ao período correspondente ao ciclo de alfabetização. Foram analisados os resultados médios em matemática dos estudantes nas três primeiras Ondas de avaliação e o percentual de acertos nos itens comuns a essas Ondas, com o intuito de verificar a evolução da aprendizagem em matemática ao longo do início da escolarização nos anos iniciais. Dentre os principais resultados da pesquisa foi possível perceber certa fragilidade na construção dos conceitos matemáticos básico dos anos iniciais, evidenciando que possivelmente a construção da linguagem matemática encontra-se aquém do esperado para os estudantes no início de sua formação matemática. Possivelmente, estes resultados reflitam uma prática comum nas escolas em que a ênfase do processo de aprendizagem esteja centrada em processos individuais, em contextos pouco familiares à criança, além da proposição de atividades que pouco exploram o raciocínio lógico e dedutivo do aluno, ou seja, o pensar sobre de forma lúdica e criativa. Tudo isso tem contribuído para aumentar a distância entre estudantes de diferentes classes sociais ou diferentes redes de ensino.

Direito internacional privado, a proteção do ser humano e a falácia do ineditismo constitucionalista e tratadista

Consensos doutrinários acerca da novidade da proteção do ser humano por declarações de direito internas e internacionais e por constituições especificamente pela constituição Brasileira de 1988 - conformaram o ponto de partida desta pesquisa. Estabeleceu-se, inicialmente, um problema teórico que buscava sistematizar no direito internacional privado o impacto da suposta revolução teórica vivenciada pelo direito nos últimos séculos entendendo-se que a doutrina conflitual brasileira não havia desenvolvido parâmetros claros aos contornos da proteção do homem em sua esfera. Cumpridos os requisitos metodológicos relacionados à apresentação de hipótese a problema específico, o aprofundamento das pesquisas mostrou-se surpreendente: a hipótese mostrava-se inconsistente. Adotou-se, assim, o prisma de sua negação. Percebeu-se que, de fato, o ser humano se encontra hoje no centro do direito, mas que no direito internacional privado a novidade anunciada não se mostrava recente e que o deslumbramento com a dignidade humana falseava na técnica conflitual sua razão de ser originária. O trabalho foi realizado levando-se em conta o método dedutivo-indutivo de pesquisa a partir da utilização das doutrinas do direito internacional privado, do discurso da proteção do homem e das teorias constitucionais como instrumento de verificação da hipótese proposta ao problema inicialmente apresentado. A inovação do estudo realizado não se encontra, assim, necessariamente em seu conteúdo, mas na sistematização teórica da relação existente entre a doutrina da proteção do indivíduo, incorporada definitivamente ao direito constitucional brasileiro atual, e o direito internacional privado. Buscou-se demonstrar que o impacto da proteção do homem na disciplina deve ser entendido como um diálogo e que a técnica conflitual não seria meramente induzida pelos direitos humanos fundamentais, mas também indutora de seu reconhecimento e consagração. O trabalho foi dividido em três partes distintas, mas interdependentes. Na primeira delas, apresentaram-se as bases teóricas da pesquisa. Foram organizadas, nesse ponto, as premissas consideradas essenciais ao avanço da investigação. A segunda seção adota a classificação predominante na doutrina brasileira para o objeto do direito internacional privado para sistematizar a análise do tema em seu viés prático. Na terceira seção, demonstra-se de que forma os resultados parciais obtidos acabaram por negar paulatinamente a hipótese inicial fixada. Observou-se que, caso se admitisse que o discurso dos direitos humanos se estabeleceu como axioma informador do direito como um todo há poucas centenas de anos e que a ordem jurídica brasileira apenas protegeu o indivíduo a partir de 1988, o direito internacional privado deveria ser entendido como predecessor, como técnica que antecipou toda essa dinâmica. Mais que isso, concluiu-se que o sobredireito internacional tem sua origem e finalidade maior na proteção dos seres humanos e que não foi apenas induzido pelo discurso da defesa do homem. Conclui-se, por fim, que tratar a proteção do ser humano pelo direito internacional privado como dado contemporâneo ou moderno constituiria, de todo o investigado, grave equívoco que desconsideraria as origens, os fundamentos e as funções da técnica conflitual.

Adolescente infrator: as práticas restaurativas (mediação) e a nova Lei do Sistema Nacional de Atendimento Socioeducativo (SINASE) na cidade do Rio de Janeiro

Este estudo, intitulado Adolescente infrator: A mediação prevista na nova Lei do Sistema Nacional de Atendimento Socioeducativo (SINASE) na cidade do Rio de Janeiro trata da mediação na vertente transformativa, com o objetivo de permitir nova ótica sobre a conduta infratora e as consequências dos atos no mundo social. Esta forma de atuação, dentre outros benefícios, pode evitar o desgaste jurisdicional, na medida em que os casos selecionados a partir de suas características passam a ser operados por especialistas em composição pacífica de conflitos, com a perspectiva de seres humanos que necessitam da inter-relação no convívio social. Os mediadores trabalham com os adolescentes em conflito com a lei, seus pais e as vítimas. Destarte, verificando as circunstâncias favoráveis à mediação, passa-se ao diálogo para alcançar um acordo, mantendo-se o centro da intervenção no conflito e na relação dos conflitantes, incentivando a capacitação para a negociação a partir do reconhecimento do direito do outro, produzindo a transformação interna dos litigantes que causará, como efeito desejado, a dissolução do conflito. A princípio os mediadores devem atuar apenas em fatos de menor potencial ofensivo, como agressões leves e outros conflitos entre adolescentes. Com o passar do tempo e o aperfeiçoamento da prática, é possível abarcar outras classes de prática infracional, a exemplo de pequenos furtos. Para tanto, na fase de pesquisa, tentando-se explicar a mediação transformadora a partir das referências teóricas publicadas em livros ou obras congêneres, utilizou-se a técnica bibliográfica; na fase da redação, ordenou-se o material coletado, segundo a lógica necessária à elaboração de um trabalho científico. O método a presidir este estudo foi o dedutivo, na medida em que parte da análise geral das crianças e dos adolescentes, em especial aqueles em conflito com a lei, para depois apresentar a teoria geral da mediação e em seguida, numa abordagem mais particular, enfrentar as questões envolvendo a mediação no Sistema Nacional de Atendimento Socioeducativo (SINASE) para, ao final, defender que é preciso desvendar o marco normativo que autoriza a prática da mediação como instrumento de resolução de questões relacionadas com o adolescente em conflito com a lei, para identificar a natureza jurídica desse modelo de mediação e, ao final, a título de sugestão, desenhar seu procedimento não estabelecido pela lei material que a prevê, qual seja, a Lei n 12.594, de 18 de janeiro de 2012. O grande desafio é establecer a metodologia adequada para que a autocomposição de conflito seja restaurativa ao adolescente infrator e aos integrantes desse conflito instaurado. O resgate do meio social abalado com a prática infracional é tão importante quanto a conscientização do adolescente. A pretensão é sugerir um marco normativo que posicione o procedimento da mediação como instrumento de ligação do indivíduo adolescente infrator, com o ambiente social onde está inserido, e com o formalismo processual que vem afastando o Poder Judiciário de sua função social de dizer o direito e fazer justiça.

A disciplina do nome empresarial: natureza e tutela jurídica

O trabalho analisa o nome empresarial como sinal revelador da personalidade do empresário individual, da sociedade empresária e da empresa individual de responsabilidade limitada. Vincula-se à linha de pesquisa Empresa e Atividades Econômicas. A pesquisa é do tipo teórico e adotou o método dedutivo, tendo objetivo analítico. As fontes utilizadas foram bibliográficas e documentais. Trata da disciplina jurídica do nome empresarial no Brasil, realizando uma evolução histórica legislativa e mostrando o aprimoramento do instituto. Descreve seu regramento jurídico atual e o distingue dos demais sinais integrantes dos elementos da empresa. Aponta as funções exercidas pelo nome empresarial. Discute a posição do nome empresarial como direito fundamental e direito da personalidade e identifica o âmbito da proteção, visando a ampliar sua abrangência material e territorial. Assinala sua proteção de forma absoluta, independentemente do ramo de atividade, e examina a respectiva tutela nos campos administrativo, civil e penal.

O impacto da cláusula de raio nas relações entre o lojista e o empreendedor e seus efeitos no direito da concorrência

A pesquisa analisa a validade da cláusula de raio no aspecto do direito civil-empresarial (privado) e da concorrência (público). No âmbito do direito civil-empresarial analisa-se a cláusula de raio em conjunto com a cláusula de aluguel percentual e possível lesão à boa-fé objetiva. No aspecto do direito da concorrência é analisado o mercado relevante na dimensão produto e geográfica, bem como as externalidades positivas e negativas produzidas pela cláusula de raio. Para a realização da pesquisa adota-se o método dedutivo, realizado a partir de pesquisa bibliográfica e jurisprudencial sobre o tema. Traz como resultado os parâmetros que devem ser utilizados para a análise da cláusula de raio e a hipótese em que ela pode ser prevista.

O fenômeno da proletarização das profissões liberais e a subordinação do contrato de trabalho

As modificações nas relações de prestação de serviço, decorrentes da sofisticação da sociedade pós-industrial, são notórias. Os trabalhadores dos dias atuais ainda são homens e mulheres que vivem da venda de sua força de trabalho, contudo, além do trabalhador operário há o surgimento de uma nova classe de trabalhadores: o trabalhador autônomo. Com isso a subordinação se tornou um importante elemento diferenciador das relações de trabalho. A visão do trabalho subordinado, um dos elementos da relação de emprego, foi construída a partir de um modelo tradicional de trabalhador. Logo, o que se pretende analisar no decorrer desta pesquisa é se o critério da subordinação presente na Consolidação das Leis do Trabalho ainda pode ser capaz de representar todas as relações de trabalho subordinada. Isto porque está se desenvolvendo uma prática de prestação de serviço na qual o profissional liberal presta o seu serviço com restrição na sua autonomia, o que denotaria a subordinação do trabalhador intelectual, mas que não se concretiza em virtude do ato formal que reveste essa relação. Estes profissionais recebem a nomenclatura de autônomo-subordinados, porque apesar de serem contratados como autônomos desempenham a sua função de modo subordinado. Esta prática possui desdobramentos negativos, como a ausência de direitos trabalhistas e previdenciários aos trabalhadores autônomo-subordinados, além da confusão social a que estão submetidos. Tais aspectos serão abordados no decorrer deste estudo, o qual utilizou como método de abordagem o dedutivo-indutivo, e também o método de procedimento bibliográfico dissertativo-argumentativo. Ao final deste trabalhou chegou-se a conclusão de que o conceito clássico de subordinação precisa ser readequado para atender a uma nova realidade do trabalho, a do trabalhador autônomo-subordinado.

面向传值进程的谓词μ-演算与FO(HML)的完备推演系统

National Natural Science Foundation of China; Public Administration and Civil Service Bureau of Macau SAR; Companhia de Telecomunicacoes de Macau S.A.R.L.; Macau SAR Government Tourist Office

学前儿童朴素生物学“理论”的发展——对“生长”认知的实验研究

There is a debate in cognitive development theory on whether cognitive development is general or specific. More and more researchers think that cognitive development is domain specific. People start to investigate preschoolers' native theory of human being's basic knowledge systems. Naive biology is one of the core domains. But there is argument whether there is separate native biological concepts among preschoolers. The research examined preschoolers' cognitive development of naive biological theory on two levels which is "growth" and "aliveness", and it also examined individual difference and factors that lead to the difference. Three studies were designed. Study 1 was to study preschoolers' cognition on growth, which is a basic trait of living things, and whether children can distinguish living and non-living things with the trait and understanding the causality. Study 2 was to investigate preschoolers' distinction between living things and non-living things from an integrated level. Study 3 was to investigate how children make inferences to unfamiliar things with their domain specific knowledge. The results showed the following: 1. Preschoolers gradually developed naive theory of biology on growth level, but their naive theory on integrated level has not developed. 2 Preschoolers' naive theory of biology is not "all or none", 4- and 5-year-old children showed some distinction between living and non-living things to some extent, they use non-intentional reason to explain the cause of growth and their explanation showed coherence. But growth has not been a criteria of ontological distinction of living and non-living things for 4- and 5-year-old children, most 6-year-old children can distinguish between living and non-living things, and these show the developing process of biological cognition. 3. Preschoolers' biological inference is influenced by their domain-specific knowledge, whether they can make inference to new trait of living things depends on whether they have specific knowledge. In the deductive task, children use their knowledge to make inference to unfamiliar things. 4-year-olds use concrete knowledge more often while the 6-year-old use generalized knowledge more frequency. 4. Preschoolers' knowledge grow with age, but individuals' cognitive development speed at different period. Urban and rural educational background affect cognitive performance. As time goes by, the urban-rural knowledge difference to distinguish living and nonliving things reduces. And preschoolers' are at the same developmental stage because the three age groups have similar causal explanation both in quantity and quality. 5. There is intra-individual difference on preschoolers' naive biological cognition. They show different performance on different tasks and domains, and their cognitive development is sequential, they understand growth earlier than they understand "alive", which is an integrated concept. The intra-individual differences decrease with age.

Type-omega DPLs

Type-omega DPLs (Denotational Proof Languages) are languages for proof presentation and search that offer strong soundness guarantees. LCF-type systems such as HOL offer similar guarantees, but their soundness relies heavily on static type systems. By contrast, DPLs ensure soundness dynamically, through their evaluation semantics; no type system is necessary. This is possible owing to a novel two-tier syntax that separates deductions from computations, and to the abstraction of assumption bases, which is factored into the semantics of the language and allows for sound evaluation. Every type-omega DPL properly contains a type-alpha DPL, which can be used to present proofs in a lucid and detailed form, exclusively in terms of primitive inference rules. Derived inference rules are expressed as user-defined methods, which are "proof recipes" that take arguments and dynamically perform appropriate deductions. Methods arise naturally via parametric abstraction over type-alpha proofs. In that light, the evaluation of a method call can be viewed as a computation that carries out a type-alpha deduction. The type-alpha proof "unwound" by such a method call is called the "certificate" of the call. Certificates can be checked by exceptionally simple type-alpha interpreters, and thus they are useful whenever we wish to minimize our trusted base. Methods are statically closed over lexical environments, but dynamically scoped over assumption bases. They can take other methods as arguments, they can iterate, and they can branch conditionally. These capabilities, in tandem with the bifurcated syntax of type-omega DPLs and their dynamic assumption-base semantics, allow the user to define methods in a style that is disciplined enough to ensure soundness yet fluid enough to permit succinct and perspicuous expression of arbitrarily sophisticated derived inference rules. We demonstrate every major feature of type-omega DPLs by defining and studying NDL-omega, a higher-order, lexically scoped, call-by-value type-omega DPL for classical zero-order natural deduction---a simple choice that allows us to focus on type-omega syntax and semantics rather than on the subtleties of the underlying logic. We start by illustrating how type-alpha DPLs naturally lead to type-omega DPLs by way of abstraction; present the formal syntax and semantics of NDL-omega; prove several results about it, including soundness; give numerous examples of methods; point out connections to the lambda-phi calculus, a very general framework for type-omega DPLs; introduce a notion of computational and deductive cost; define several instrumented interpreters for computing such costs and for generating certificates; explore the use of type-omega DPLs as general programming languages; show that DPLs do not have to be type-less by formulating a static Hindley-Milner polymorphic type system for NDL-omega; discuss some idiosyncrasies of type-omega DPLs such as the potential divergence of proof checking; and compare type-omega DPLs to other approaches to proof presentation and discovery. Finally, a complete implementation of NDL-omega in SML-NJ is given for users who want to run the examples and experiment with the language.

Dependency Directed Reasoning for Complex Program Understanding

Artificial Intelligence research involves the creation of extremely complex programs which must possess the capability to introspect, learn, and improve their expertise. Any truly intelligent program must be able to create procedures and to modify them as it gathers information from its experience. [Sussman, 1975] produced such a system for a 'mini-world'; but truly intelligent programs must be considerably more complex. A crucial stepping stone in AI research is the development of a system which can understand complex programs well enough to modify them. There is also a complexity barrier in the world of commercial software which is making the cost of software production and maintenance prohibitive. Here too a system which is capable of understanding complex programs is a necessary step. The Programmer's Apprentice Project [Rich and Shrobe, 76] is attempting to develop an interactive programming tool which will help expert programmers deal with the complexity involved in engineering a large software system. This report describes REASON, the deductive component of the programmer's apprentice. REASON is intended to help expert programmers in the process of evolutionary program design. REASON utilizes the engineering techniques of modelling, decomposition, and analysis by inspection to determine how modules interact to achieve the desired overall behavior of a program. REASON coordinates its various sources of knowledge by using a dependency-directed structure which records the justification for each deduction it makes. Once a program has been analyzed these justifications can be summarized into a teleological structure called a plan which helps the system understand the impact of a proposed program modification.

SIR: A Computer Program for Semantic Information Retrieval

SIR is a computer system, programmed in the LISP language, which accepts information and answers questions expressed in a restricted form of English. This system demonstrates what can reasonably be called an ability to "understand" semantic information. SIR's semantic and deductive ability is based on the construction of an internal model, which uses word associations and property lists, for the relational information normally conveyed in conversational statements. A format-matching procedure extracts semantic content from English sentences. If an input sentence is declarative, the system adds appropriate information to the model. If an input sentence is a question, the system searches the model until it either finds the answer or determines why it cannot find the answer. In all cases SIR reports its conclusions. The system has some capacity to recognize exceptions to general rules, resolve certain semantic ambiguities, and modify its model structure in order to save computer memory space. Judging from its conversational ability, SIR, is a first step toward intelligent man-machine communication. The author proposes a next step by describing how to construct a more general system which is less complex and yet more powerful than SIR. This proposed system contains a generalized version of the SIR model, a formal logical system called SIR1, and a computer program for testing the truth of SIR1 statements with respect to the generalized model by using partial proof procedures in the predicate calculus. The thesis also describes the formal properties of SIR1 and how they relate to the logical structure of SIR.

Description and Theoretical Analysis (Using Schemata) of Planner: A Language for Proving Theorems and Manipulating Models in a Robot

Planner is a formalism for proving theorems and manipulating models in a robot. The formalism is built out of a number of problem-solving primitives together with a hierarchical multiprocess backtrack control structure. Statements can be asserted and perhaps later withdrawn as the state of the world changes. Under BACKTRACK control structure, the hierarchy of activations of functions previously executed is maintained so that it is possible to revert to any previous state. Thus programs can easily manipulate elaborate hypothetical tentative states. In addition PLANNER uses multiprocessing so that there can be multiple loci of changes in state. Goals can be established and dismissed when they are satisfied. The deductive system of PLANNER is subordinate to the hierarchical control structure in order to maintain the desired degree of control. The use of a general-purpose matching language as the basis of the deductive system increases the flexibility of the system. Instead of explicitly naming procedures in calls, procedures can be invoked implicitly by patterns of what the procedure is supposed to accomplish. The language is being applied to solve problems faced by a robot, to write special purpose routines from goal oriented language, to express and prove properties of procedures, to abstract procedures from protocols of their actions, and as a semantic base for English.