Theorem Proving
Mostrando 1-12 de 14 artigos, teses e dissertações.
-
1. Coefficient modules in algebras / Módulos coeficientes em álgebras
In 1991, Kishor Shah defined and studied coeficient ideals I ind {k}. , for integers k = 0, . . . , d, associated to an ideal m-primary I of a Noetherian local ring of dimension, (R,m). This ideals, I ind {k}. , are the biggest ideals of R that contains the ideal I such that the first k+1 Hilbert-Samuel coefficients of I and I IND. {k}are igual. The main res
Publicado em: 2010
-
2. Relational approach of graph grammars / Abordagem relacional de gramática de grafos
Gramática de grafos é uma linguagem formal bastante adequada para sistemas cujos estados possuem uma topologia complexa (que envolvem vários tipos de elementos e diferentes tipos de relações entre eles) e cujo comportamento é essencialmente orientado pelos dados, isto é, eventos são disparados por configurações particulares do estado. Vários siste
Publicado em: 2010
-
3. Component assembly and theorem proving in constraint handling rules
Devido à grande demanda por softwares cada vez mais robustos, complexos e flexÃveis, e, sobretudo, pelo curtÃssimo tempo de entrega exigido, a engenharia de software tem procurado novos meios de desenvolvimento que supram satisfatoriamente essas demandas. Uma forma de galgar esses novos patamares de produtividade provÃm do uso de uma metodologia baseada
Publicado em: 2009
-
4. Argumentação e prova: explorações a partir da análise de uma coleção didática
This work is inserted the research project Argumentation and Proof in School Mathematics (AProvaME), which aims to study the teaching and learning of mathematical proofs during compulsory schooling. The main research question of this contribution to the project relates to how proof is treated in particular geometry topics in one collection of mathematics tex
Publicado em: 2007
-
5. A refinement theory for alloy / A refinement theory for alloy
Refatoramentos sÃo geralmente propostos de maneira ad hoc, porque à difÃcil provar formalmente que eles preservam comportamento. Na prÃtica, desenvolvedores, mesmo utilizando ferramentas de refatoramento, tÃm que usar compilaÃÃo e testes para garantir que os refatoramentos sÃo corretos. Esse cenÃrio nÃo à desejado principalmente no desenvolvimento
Publicado em: 2007
-
6. Simetrias de hipersuperfÃcies com curvatura escalar nula via PrincÃpio da TangÃncia
In 1983, R. Schoen proved that the only complete immersed minimal hypersurfaces in Rn+1 with two regular ends are the catenoid and a pair of planes. The methods used by Schoen led J. Hounie and M. L. Leite to prove a similar result for hypersurfaces with zero scalar curvature. The main difference in the proof of the two theorems is in the fact that the equat
Publicado em: 2005
-
7. Hierarquias de sistemas de dedução natural e de sistemas de tableaux analiticos para os sistemas Cn de da Costa
In this work, we introduce the hierarchy of propositional natural deduction systems DNCn, 1≤n≤ω, and the hierarchy of quantificational natural deduction systems DNCn*, 1≤n≤ω. We prove that each one of the systems of the hierarchies is equivalent to the corresponding system of the hierarchy of da Costa´s propositional paraco
Publicado em: 2004
-
8. Contribuições para verificação automática de applets javacard
O grande crescimento do uso de smart cards (por bancos, companhias de transporte, celulares, etc) trouxe um fato importante, que deve ser considerado: a necessidade de ferramentas que possam ser usadas para verificar os cartões, para que se possa garantir a corretude de seu software. Como a grande maioria dos cartões desenvolvidos hoje em dia usa a t
Publicado em: 2004
-
9. Scalable automated proving and debugging of set-based specifications
We present a technique to prove invariants of model-based specifications in a fragment of set theory. Proof obligations containing set theory constructs are translated to first-order logic with equality augmented with (an extension of) the theory of arrays with extensionality. The idea underlying the translation is that sets are represented by their characte
Journal of the Brazilian Computer Society. Publicado em: 2003-11
-
10. TECHNIQUES FOR THE USE OF HOARE LOGIC IN PCC / TÉCNICAS PARA O USO DO CÁLCULO DE HOARE EM PCC
Atualmente, a maioria dos programas para computadores é obtida através da WEB. Como muitas vezes a procedência são fontes desconhecidas, é preciso se certificar de que o código se comporta como o esperado. A solução ideal seria verificar o código contra uma especificação de políticas de segurança ,contudo, isso pode consumir muito tempo.Uma outr
Publicado em: 2003
-
11. Hipersuperficies de coomogeneidade um na esfera euclidiana
In 1994, Podestà and Spiro proved that a compact hypersurface of cohomogeneity one, f : Mn + IRn+1, n _ 4, whose principal orbits are umbilical in M is a hyper surface ofrevolution. In 1996, in his Ph.D. thesis, Seixas weakened the hypothesis of this theorem, proving the result for complete hypersurfaces and extended the result of Podestà and Spiro to the
Publicado em: 2002
-
12. Algebraic theory for the clique operator
In this text we attempt to unify many results about the K operator based on a new theory involving graphs, families and operators. We are able to build an ''operator algebra'' that helps to unify and automate arguments. In addition, we relate well-known properties, such as the Helly property, to the families and the operators. As a result, we deduce many cla
Journal of the Brazilian Computer Society. Publicado em: 2001